# HG changeset patch # User wenzelm # Date 1014920594 -3600 # Node ID 8f717cbd4e44a1e839b74e2a6a1fe357046a3ca5 # Parent 4c76bce4ce391d6e2b8e938ccf65925279426aaf rewrite_term: Term.rename_abs; diff -r 4c76bce4ce39 -r 8f717cbd4e44 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Thu Feb 28 19:22:56 2002 +0100 +++ b/src/Pure/pattern.ML Thu Feb 28 19:23:14 2002 +0100 @@ -420,7 +420,8 @@ in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end; fun match_rew tm (tm1, tm2) = - Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None; + Some (subst_vars (match tsig (tm1, tm)) (if_none (Term.rename_abs tm1 tm tm2) tm2)) + handle MATCH => None; fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body)) | rew tm = get_first (match_rew tm) rules;