@@ -120,7 +120,8 @@ get_instances = do ES p _ _ <- get
120120unique_hole :: Name -> Elab Name
121121unique_hole n = do ES p _ _ <- get
122122 let bs = bound_in (pterm p) ++ bound_in (ptype p)
123− return (uniqueName n (holes p ++ bs))
123+ n' <- uniqueNameCtxt (context p) n (holes p ++ bs)
124+ return n'
124125 where
125126 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
126127 where
@@ -130,6 +131,12 @@ unique_hole n = do ES p _ _ <- get
130131 bound_in (App f a) = bound_in f ++ bound_in a
131132 bound_in _ = []
132133
134+uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name
135+uniqueNameCtxt ctxt n hs
136+ | n `elem` hs = return $ uniqueName (nextName n) hs
137+ | Just _ <- lookupCtxt n ctxt = return $ uniqueName (nextName n) hs
138+ | otherwise = return n
139+
133140elog :: String -> Elab ()
134141elog str = do ES p logs prev <- get
135142 put (ES p (logs ++ str ++ "\n") prev)