@@ -20,6 +20,7 @@ import Idris.CaseSplit
20import Idris.AbsSyntax
20import Idris.AbsSyntax
21import Idris.ElabDecls
21import Idris.ElabDecls
22import Idris.Error
22import Idris.Error
23+import Idris.ErrReverse
23import Idris.Delaborate
24import Idris.Delaborate
24import Idris.Output
25import Idris.Output
25import Idris.IdeMode hiding (IdeModeCommand(..))
26import Idris.IdeMode hiding (IdeModeCommand(..))
@@ -333,11 +334,14 @@ makeLemma fn updatefile l n
333 let isProv = checkProv tyline (show n)
334 let isProv = checkProv tyline (show n)
335 ctxt <- getContext
336 ctxt <- getContext
336− (fname, mty) <- case lookupTyName n ctxt of
337+ (fname, mty_full) <- case lookupTyName n ctxt of
337− [t] -> return t
338+ [t] -> return t
338− [] -> ierror (NoSuchVariable n)
339+ [] -> ierror (NoSuchVariable n)
339− ns -> ierror (CantResolveAlts (map fst ns))
340+ ns -> ierror (CantResolveAlts (map fst ns))
340 i <- getIState
342 i <- getIState
343+ let mty = errReverse i mty_full
341 margs <- case lookup fname (idris_metavars i) of
345 margs <- case lookup fname (idris_metavars i) of
342 Just (_, arity, _, _, _) -> return arity
346 Just (_, arity, _, _, _) -> return arity
343 _ -> return (-1)
347 _ -> return (-1)