@@ -100,11 +100,14 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
100100 | n == eqTy = PEq un (de env [] l) (de env [] r)
101101 | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder
102102 (de env [] r)
103− deFn env (P _ n _) args | not mvs
104− = case lookup n (idris_metavars ist) of
105− Just (Just _, mi, _) ->
106− mkMVApp n (drop mi (map (de env []) args))
107− _ -> mkPApp n (map (de env []) args)
103+ deFn env f@(P _ n _) args
104+ | n `elem` map snd env
105+ = PApp un (de env [] f) (map pexp (map (de env []) args))
106+ deFn env (P _ n _) args
107+ | not mvs = case lookup n (idris_metavars ist) of
108+ Just (Just _, mi, _) ->
109+ mkMVApp n (drop mi (map (de env []) args))
110+ _ -> mkPApp n (map (de env []) args)
108111 | otherwise = mkPApp n (map (de env []) args)
109112 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
110113
@@ -113,7 +116,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
113116 mkMVApp n args
114117 = PApp un (PMetavar n) (map pexp args)
115118 mkPApp n args
116− | [imps] <- lookupCtxt n (idris_implicits ist)
119+ | Just imps <- lookupCtxtExact n (idris_implicits ist)
117120 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
118121 | otherwise = PApp un (PRef un n) (map pexp args)
119122