@@ -51,6 +51,8 @@ names over '_', patterns over names, etc.
51split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
51split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
53 = do ist <- getIState
53 = do ist <- getIState
54+ -- Make sure all the names in the term are accessible
55+ mapM_ (\n -> setAccessibility n Public) (allNamesIn t')
54 (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
56 (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
55 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
57 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
56-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
58-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))