1.1 --- a/src/HOL/Library/reflection.ML	Thu Jun 09 22:25:25 2011 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Thu Jun 09 23:12:02 2011 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4                   map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
     1.5                val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
     1.6              in ((fts ~~ (replicate (length fts) ctxt),
     1.7 -                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
     1.8 +                 Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
     1.9              end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
    1.10        end;
    1.11  
    1.12 @@ -230,7 +230,7 @@
    1.13              val substt =
    1.14                let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
    1.15                in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts)  end
    1.16 -            val th = (instantiate (subst_ty, substt)  eq) RS sym
    1.17 +            val th = (Drule.instantiate_normalize (subst_ty, substt)  eq) RS sym
    1.18            in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
    1.19            handle Pattern.MATCH => tryeqs eqs bds)
    1.20        in tryeqs (filter isat eqs) bds end), bds);
    1.21 @@ -277,7 +277,7 @@
    1.22      val cert = cterm_of (Proof_Context.theory_of ctxt)
    1.23      val cvs = map (fn (v as Var(n,t)) => (cert v,
    1.24                    the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
    1.25 -    val th' = instantiate ([], cvs) th
    1.26 +    val th' = Drule.instantiate_normalize ([], cvs) th
    1.27      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
    1.28      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
    1.29                 (fn _ => simp_tac (simpset_of ctxt) 1)