@@ -157,13 +157,25 @@ mergeAllPats ist cv t (p : ps)
157157 patvars _ = []
158158
159159mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
160+mergePat ist orig new t =
161+ do -- collect user names for name map, by matching user pattern against
162+ -- the generated pattern
163+ case matchClause ist orig new of
164+ Left _ -> return ()
165+ Right ns -> mapM_ addNameMap ns
166+ mergePat' ist orig new t
167+ where
168+ addNameMap (n, PRef fc _ n') = do ms <- get
169+ put (ms { namemap = ((n', n) : namemap ms) })
170+ addNameMap _ = return ()
171+
160172-- If any names are unified, make sure they stay unified. Always prefer
161173-- user provided name (first pattern)
162−mergePat ist (PPatvar fc n) new t
163− = mergePat ist (PRef fc [] n) new t
164−mergePat ist old (PPatvar fc n) t
165− = mergePat ist old (PRef fc [] n) t
166−mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t
174+mergePat' ist (PPatvar fc n) new t
175+ = mergePat' ist (PRef fc [] n) new t
176+mergePat' ist old (PPatvar fc n) t
177+ = mergePat' ist old (PRef fc [] n) t
178+mergePat' ist orig@(PRef fc _ n) new@(PRef _ _ n') t
167179 | isDConName n' (tt_ctxt ist) = do addUpdate n new
168180 return new
169181 | otherwise
@@ -173,20 +185,20 @@ mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t
173185 return (PRef fc [] x)
174186 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
175187 return (PRef fc [] n)
176−mergePat ist (PApp _ _ args) (PApp fc f args') t
188+mergePat' ist (PApp _ _ args) (PApp fc f args') t
177189 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
178190 return (PApp fc f newArgs)
179191 where mergeArg x (y, t)
180− = do tm' <- mergePat ist (getTm x) (getTm y) t
192+ = do tm' <- mergePat' ist (getTm x) (getTm y) t
181193 case x of
182194 (PImp _ _ _ _ _) ->
183195 return (y { machine_inf = machine_inf x,
184196 getTm = tm' })
185197 _ -> return (y { getTm = tm' })
186−mergePat ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
187− addUpdate n tm
188− return tm
189−mergePat ist x y t = return y
198+mergePat' ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
199+ addUpdate n tm
200+ return tm
201+mergePat' ist x y t = return y
190202
191203mergeUserImpl :: PTerm -> PTerm -> PTerm
192204mergeUserImpl x y = x