rewrite_term: Term.rename_abs;
authorwenzelm
Thu Feb 28 19:23:14 2002 +0100 (2002-02-28)
changeset 129808f717cbd4e44
parent 12979 4c76bce4ce39
child 12981 f48de47c32d6
rewrite_term: Term.rename_abs;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Thu Feb 28 19:22:56 2002 +0100
     1.2 +++ b/src/Pure/pattern.ML	Thu Feb 28 19:23:14 2002 +0100
     1.3 @@ -420,7 +420,8 @@
     1.4        in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
     1.5  
     1.6      fun match_rew tm (tm1, tm2) =
     1.7 -      Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None;
     1.8 +      Some (subst_vars (match tsig (tm1, tm)) (if_none (Term.rename_abs tm1 tm tm2) tm2))
     1.9 +        handle MATCH => None;
    1.10      fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
    1.11        | rew tm = get_first (match_rew tm) rules;
    1.12