@@ -2218,17 +2218,20 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
22182218substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
22192219substMatches ms = substMatchesShadow ms []
22202220
2221−substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2222−substMatchesShadow [] shs t = t
2223−substMatchesShadow ((n,tm):ns) shs t
2224− = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2221+-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2222+-- substMatchesShadow [] shs t = t
2223+-- substMatchesShadow ((n,tm):ns) shs t
2224+-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
22252225
22262226substMatch :: Name -> PTerm -> PTerm -> PTerm
22272227substMatch n = substMatchShadow n []
22282228
22292229substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2230−substMatchShadow n shs tm t = sm shs t where
2231− sm xs (PRef _ _ n') | n == n' = tm
2230+substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2231+
2232+substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2233+substMatchesShadow nmap shs t = sm shs t where
2234+ sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
22322235 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
22332236 sm xs (PPi p x fc t sc)
22342237 | x `elem` xs