src/HOL/Tools/TFL/thry.ML
changeset 32035 8e77b6a250d5
parent 31784 bd3486c57ba3
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/TFL/thry.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/thry.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  fun match_term thry pat ob =
     1.5    let
     1.6      val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
     1.7 -    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
     1.8 +    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
     1.9    in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
    1.10    end;
    1.11