src/Pure/pattern.ML
changeset 32035 8e77b6a250d5
parent 32032 a6a6e8031c14
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/pattern.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -354,7 +354,7 @@
     1.4        Abs(ns,Ts,ts) =>
     1.5          (case obj of
     1.6             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
     1.7 -         | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
     1.8 +         | _ => let val Tt = Envir.subst_type iTs Ts
     1.9                  in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
    1.10      | _ => (case obj of
    1.11                Abs(nt,Tt,tt) =>
    1.12 @@ -428,7 +428,7 @@
    1.13  
    1.14  fun match_rew thy tm (tm1, tm2) =
    1.15    let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
    1.16 -    SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
    1.17 +    SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
    1.18        handle MATCH => NONE
    1.19    end;
    1.20