@@ -241,7 +241,7 @@ elab ist info pattern tcgen fn tm
241241 let fty = fnTy argTys rty
242242-- trace (show (ptm, map fst argTys)) $ focus fn
243243 -- build and defer the function application
244− attack; deferType f fty (map fst argTys); solve
244+ attack; deferType (mkN f) fty (map fst argTys); solve
245245 -- elaborate the arguments, to unify their types. They all have to
246246 -- be explicit.
247247 mapM_ elabIArg (zip argTys args)
@@ -261,6 +261,11 @@ elab ist info pattern tcgen fn tm
261261
262262 elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
263263 elabIArg _ = return () -- already done, just a name
264+
265+ mkN n@(NS _ _) = n
266+ mkN n = case namespace info of
267+ Just xs@(_:_) -> NS n xs
268+ _ -> n
264269
265270 elab' (ina, g) tm@(PApp fc (PRef _ f) args')
266271 = do let args = {- case lookupCtxt f (inblock info) of