@@ -1202,7 +1202,10 @@ toEither (RightOK ho) = Right ho
12021202-- and what they match. Returns the pair that failed if not a match.
12031203
12041204matchClause :: PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1205−matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where
1205+matchClause = matchClause' False
1206+
1207+matchClause' :: Bool -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1208+matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where
12061209 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
12071210
12081211 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
@@ -1219,7 +1222,7 @@ matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where
12191222 match (PRef f n) (PApp _ x []) = match (PRef f n) x
12201223 match (PApp _ x []) (PRef f n) = match x (PRef f n)
12211224 match (PRef _ n) (PRef _ n') | n == n' = return []
1222− match (PRef _ n) tm = return [(n, tm)]
1225+ match (PRef _ n) tm | not names = return [(n, tm)]
12231226 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
12241227 mr <- match' r r'
12251228 return (ml ++ mr)