@@ -1323,7 +1323,7 @@ substMatchShadow n shs tm t = sm shs t where
13231323 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
13241324 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
13251325 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1326− sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)
1326+ sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
13271327 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
13281328 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
13291329 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
@@ -1336,6 +1336,9 @@ substMatchShadow n shs tm t = sm shs t where
13361336 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
13371337 sm xs x = x
13381338
1339+ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1340+ fullApp x = x
1341+
13391342shadow :: Name -> Name -> PTerm -> PTerm
13401343shadow n n' t = sm t where
13411344 sm (PRef fc x) | n == x = PRef fc n'