@@ -696,6 +696,10 @@ elab ist info emode opts fn tm
696 letbind scvn (Var tyn) (Var valn)
696 letbind scvn (Var tyn) (Var valn)
697 focus valn
697 focus valn
698 elabE (True, a, inty, qq) scr
698 elabE (True, a, inty, qq) scr
699+ -- Solve any remaining implicits - we need to solve as many
700+ -- as possible before making the 'case' type
699 args <- get_env
703 args <- get_env
700 envU <- mapM (getKind args) args
704 envU <- mapM (getKind args) args
701 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
705 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts