1.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -205,8 +205,8 @@
     1.4              val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
     1.5              val rhs_P = subst_free subst rhs
     1.6              val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
     1.7 -            val sbst = Envir.subst_vars (tyenv, tmenv)
     1.8 -            val sbsT = Envir.typ_subst_TVars tyenv
     1.9 +            val sbst = Envir.subst_term (tyenv, tmenv)
    1.10 +            val sbsT = Envir.subst_type tyenv
    1.11              val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
    1.12                                 (Vartab.dest tyenv)
    1.13              val tml = Vartab.dest tmenv