@@ -868,9 +868,13 @@ elab ist info emode opts fn tm
868868 envU <- mapM (getKind args) args
869869 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
870870
871− -- Drop the unique arguments used in the scrutinee (since it's
872− -- not valid to use them again anyway)
873− let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)
871+ -- Drop the unique arguments used in the term already
872+ -- and in the scrutinee (since it's
873+ -- not valid to use them again anyway)
874+ ptm <- get_term
875+ let argsDropped = filter (isUnique envU)
876+ (nub $ allNamesIn scr ++ inApp ptm)
877+
874878 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
875879
876880 cname <- unique_hole' True (mkCaseName fn)
@@ -897,6 +901,13 @@ elab ist info emode opts fn tm
897901 Just xs@(_:_) -> sNS n xs
898902 _ -> n
899903
904+ inApp (P _ n _) = [n]
905+ inApp (App f a) = inApp f ++ inApp a
906+ inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
907+ inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
908+ inApp (Bind n b sc) = inApp sc
909+ inApp _ = []
910+
900911 isUnique envk n = case lookup n envk of
901912 Just u -> u
902913 _ -> False