1.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -153,8 +153,8 @@
     1.4              val certy = ctyp_of thy
     1.5              val (tyenv, tmenv) =
     1.6                Pattern.match thy
     1.7 -              ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
     1.8 -              (Envir.type_env (Envir.empty 0), Vartab.empty)
     1.9 +                ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    1.10 +                (Vartab.empty, Vartab.empty)
    1.11              val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
    1.12              val (fts,its) =
    1.13  	      (map (snd o snd) fnvs,
    1.14 @@ -204,9 +204,7 @@
    1.15              val xns_map = (fst (split_list nths)) ~~ xns
    1.16              val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
    1.17              val rhs_P = subst_free subst rhs
    1.18 -            val (tyenv, tmenv) = Pattern.match
    1.19 -                              thy (rhs_P, t)
    1.20 -                              (Envir.type_env (Envir.empty 0), Vartab.empty)
    1.21 +            val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
    1.22              val sbst = Envir.subst_vars (tyenv, tmenv)
    1.23              val sbsT = Envir.typ_subst_TVars tyenv
    1.24              val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))