src/HOL/Library/rewrite.ML
changeset 60642 48dd1cefb4ae
parent 60122 eb08fefd5c05
child 61476 1884c40f1539
     1.1 --- a/src/HOL/Library/rewrite.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -265,15 +265,13 @@
     1.4    let
     1.5      fun instantiate_normalize_env ctxt env thm =
     1.6        let
     1.7 -        fun certs f = map (apply2 (f ctxt))
     1.8          val prop = Thm.prop_of thm
     1.9          val norm_type = Envir.norm_type o Envir.type_env
    1.10          val insts = Term.add_vars prop []
    1.11 -          |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
    1.12 -          |> certs Thm.cterm_of
    1.13 +          |> map (fn x as (s, T) =>
    1.14 +              ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
    1.15          val tyinsts = Term.add_tvars prop []
    1.16 -          |> map (fn x => (TVar x, norm_type env (TVar x)))
    1.17 -          |> certs Thm.ctyp_of
    1.18 +          |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
    1.19        in Drule.instantiate_normalize (tyinsts, insts) thm end
    1.20      
    1.21      fun unify_with_rhs context to env thm =