@@ -1323,7 +1323,7 @@ substMatchShadow n shs tm t = sm shs t where
1323 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
1323 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
1324 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
1324 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
1325 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1325 | 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)
1327 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1327 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1328 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1328 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1329 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1329 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
1336 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1336 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1337 sm xs x = x
1337 sm xs x = x
1339+ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1339shadow :: Name -> Name -> PTerm -> PTerm
1342shadow :: Name -> Name -> PTerm -> PTerm
1340shadow n n' t = sm t where
1343shadow n n' t = sm t where
1341 sm (PRef fc x) | n == x = PRef fc n'
1344 sm (PRef fc x) | n == x = PRef fc n'