src/HOL/Library/reflection.ML
changeset 32035 8e77b6a250d5
parent 32032 a6a6e8031c14
child 32149 ef59550a55d3
--- a/src/HOL/Library/reflection.ML	Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Library/reflection.ML	Fri Jul 17 23:11:40 2009 +0200
@@ -205,8 +205,8 @@
             val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
             val rhs_P = subst_free subst rhs
             val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
-            val sbst = Envir.subst_vars (tyenv, tmenv)
-            val sbsT = Envir.typ_subst_TVars tyenv
+            val sbst = Envir.subst_term (tyenv, tmenv)
+            val sbsT = Envir.subst_type tyenv
             val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
                                (Vartab.dest tyenv)
             val tml = Vartab.dest tmenv