src/Pure/pattern.ML
changeset 12980 8f717cbd4e44
parent 12826 dfb214fa310b
child 13195 98975cc13d28
equal deleted inserted replaced
12979:4c76bce4ce39 12980:8f717cbd4e44
   418         val x' = variant (add_term_free_names (t, rhs_names)) x;
   418         val x' = variant (add_term_free_names (t, rhs_names)) x;
   419         val t' = subst_bound (Free (x', T), t);
   419         val t' = subst_bound (Free (x', T), t);
   420       in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
   420       in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
   421 
   421 
   422     fun match_rew tm (tm1, tm2) =
   422     fun match_rew tm (tm1, tm2) =
   423       Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None;
   423       Some (subst_vars (match tsig (tm1, tm)) (if_none (Term.rename_abs tm1 tm tm2) tm2))
       
   424         handle MATCH => None;
   424     fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
   425     fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
   425       | rew tm = get_first (match_rew tm) rules;
   426       | rew tm = get_first (match_rew tm) rules;
   426 
   427 
   427     fun rew1 tm = (case rew2 tm of
   428     fun rew1 tm = (case rew2 tm of
   428           Some tm1 => (case rew tm1 of
   429           Some tm1 => (case rew tm1 of