tuned -- more explicit use of context;
authorwenzelm
Fri Mar 06 00:00:57 2015 +0100 (2015-03-06)
changeset 59617b60e65ad13df
parent 59616 eb59c6968219
child 59618 e6939796717e
tuned -- more explicit use of context;
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/record.ML
src/HOL/Tools/reification.ML
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Mar 05 13:28:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Mar 06 00:00:57 2015 +0100
     1.3 @@ -213,11 +213,13 @@
     1.4  
     1.5  fun cterm_instantiate_pos cts thm =
     1.6    let
     1.7 -    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
     1.8 +    val thy = Thm.theory_of_thm thm;
     1.9      val vars = Term.add_vars (Thm.prop_of thm) [];
    1.10      val vars' = rev (drop (length vars - length cts) vars);
    1.11 -    val ps = map_filter (fn (_, NONE) => NONE
    1.12 -      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
    1.13 +    val ps =
    1.14 +      map_filter
    1.15 +        (fn (_, NONE) => NONE
    1.16 +          | (var, SOME ct) => SOME (Thm.cterm_of thy (Var var), ct)) (vars' ~~ cts);
    1.17    in
    1.18      Drule.cterm_instantiate ps thm
    1.19    end;
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Mar 05 13:28:04 2015 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 00:00:57 2015 +0100
     2.3 @@ -352,10 +352,10 @@
     2.4  in  
     2.5    fun freeze_spec th ctxt =
     2.6      let
     2.7 -      val cert = Proof_Context.cterm_of ctxt;
     2.8        val ([x], ctxt') =
     2.9          Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
    2.10 -      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
    2.11 +      val spec' = spec
    2.12 +        |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
    2.13      in (th RS spec', ctxt') end
    2.14  end;
    2.15  
     3.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 05 13:28:04 2015 +0100
     3.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Mar 06 00:00:57 2015 +0100
     3.3 @@ -398,21 +398,19 @@
     3.4    (case Thm.tpairs_of th of
     3.5      [] => th
     3.6    | pairs =>
     3.7 -    let
     3.8 -      val thy = Thm.theory_of_thm th
     3.9 -      val cert = Thm.cterm_of thy
    3.10 -      val certT = Thm.ctyp_of thy
    3.11 -      val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
    3.12 -
    3.13 -      fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
    3.14 -      fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
    3.15 -
    3.16 -      val instsT = Vartab.fold (cons o mkT) tyenv []
    3.17 -      val insts = Vartab.fold (cons o mk) tenv []
    3.18 -    in
    3.19 -      Thm.instantiate (instsT, insts) th
    3.20 -    end
    3.21 -    handle THM _ => th)
    3.22 +      let
    3.23 +        val thy = Thm.theory_of_thm th
    3.24 +        val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
    3.25 +  
    3.26 +        fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (v, S), T)
    3.27 +        fun mk (v, (T, t)) = apply2 (Thm.cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
    3.28 +  
    3.29 +        val instsT = Vartab.fold (cons o mkT) tyenv []
    3.30 +        val insts = Vartab.fold (cons o mk) tenv []
    3.31 +      in
    3.32 +        Thm.instantiate (instsT, insts) th
    3.33 +      end
    3.34 +      handle THM _ => th)
    3.35  
    3.36  fun is_metis_literal_genuine (_, (s, _)) =
    3.37    not (String.isPrefix class_prefix (Metis_Name.toString s))
     4.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Mar 05 13:28:04 2015 +0100
     4.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Mar 06 00:00:57 2015 +0100
     4.3 @@ -609,8 +609,6 @@
     4.4      val (indrule_lemma_prems, indrule_lemma_concls) =
     4.5        split_list (map2 mk_indrule_lemma descr' recTs);
     4.6  
     4.7 -    val cert = Thm.cterm_of thy6;
     4.8 -
     4.9      val indrule_lemma =
    4.10        Goal.prove_sorry_global thy6 [] []
    4.11          (Logic.mk_implies
    4.12 @@ -627,7 +625,8 @@
    4.13      val frees =
    4.14        if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
    4.15        else map (Free o apfst fst o dest_Var) Ps;
    4.16 -    val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
    4.17 +    val indrule_lemma' =
    4.18 +      cterm_instantiate (map (Thm.cterm_of thy6) Ps ~~ map (Thm.cterm_of thy6) frees) indrule_lemma;
    4.19  
    4.20      val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
    4.21      val dt_induct =
     5.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Thu Mar 05 13:28:04 2015 +0100
     5.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Mar 06 00:00:57 2015 +0100
     5.3 @@ -126,7 +126,7 @@
     5.4  
     5.5  fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
     5.6    let
     5.7 -    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
     5.8 +    val thy = Thm.theory_of_cterm cgoal;
     5.9      val goal = Thm.term_of cgoal;
    5.10      val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule));
    5.11      val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
    5.12 @@ -148,7 +148,8 @@
    5.13        map_filter (fn (t, u) =>
    5.14          (case abstr (getP u) of
    5.15            NONE => NONE
    5.16 -        | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
    5.17 +        | SOME u' =>
    5.18 +            SOME (apply2 (Thm.cterm_of thy) (t |> getP |> snd |> head_of, u')))) (ts ~~ ts');
    5.19      val indrule' = cterm_instantiate insts indrule;
    5.20    in resolve0_tac [indrule'] i end);
    5.21  
    5.22 @@ -157,7 +158,6 @@
    5.23  
    5.24  fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
    5.25    let
    5.26 -    val thy = Thm.theory_of_cterm cgoal;
    5.27      val goal = Thm.term_of cgoal;
    5.28      val params = Logic.strip_params goal;
    5.29      val (_, Type (tname, _)) = hd (rev params);
    5.30 @@ -166,8 +166,8 @@
    5.31      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    5.32      val exhaustion' =
    5.33        cterm_instantiate
    5.34 -        [(Thm.cterm_of thy (head_of lhs),
    5.35 -          Thm.cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
    5.36 +        [apply2 (Proof_Context.cterm_of ctxt)
    5.37 +          (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
    5.38          exhaustion;
    5.39    in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
    5.40  
     6.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Mar 05 13:28:04 2015 +0100
     6.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Fri Mar 06 00:00:57 2015 +0100
     6.3 @@ -46,8 +46,7 @@
     6.4            Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
     6.5              Var (("P", 0), HOLogic.boolT));
     6.6          val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
     6.7 -        val cert = Thm.cterm_of thy;
     6.8 -        val insts' = map cert induct_Ps ~~ map cert insts;
     6.9 +        val insts' = map (Thm.cterm_of thy) induct_Ps ~~ map (Thm.cterm_of thy) insts;
    6.10          val induct' =
    6.11            refl RS
    6.12              (nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
    6.13 @@ -204,11 +203,12 @@
    6.14              Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
    6.15                absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
    6.16                  (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
    6.17 -        val cert = Thm.cterm_of thy1;
    6.18          val insts =
    6.19            map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
    6.20              ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
    6.21 -        val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
    6.22 +        val induct' = induct
    6.23 +          |> cterm_instantiate
    6.24 +            (map (Thm.cterm_of thy1) induct_Ps ~~ map (Thm.cterm_of thy1) insts);
    6.25        in
    6.26          Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
    6.27            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
    6.28 @@ -379,9 +379,9 @@
    6.29  
    6.30      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
    6.31        let
    6.32 -        val cert = Thm.cterm_of thy;
    6.33          val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
    6.34 -        val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
    6.35 +        val exhaustion' = exhaustion
    6.36 +          |> cterm_instantiate [apply2 (Thm.cterm_of thy) (lhs, Free ("x", T))];
    6.37          fun tac ctxt =
    6.38            EVERY [resolve_tac ctxt [exhaustion'] 1,
    6.39              ALLGOALS (asm_simp_tac
    6.40 @@ -450,10 +450,10 @@
    6.41        let
    6.42          val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
    6.43          val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
    6.44 -        val cert = Thm.cterm_of thy;
    6.45          val nchotomy' = nchotomy RS spec;
    6.46          val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
    6.47 -        val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
    6.48 +        val nchotomy'' =
    6.49 +          cterm_instantiate [apply2 (Thm.cterm_of thy) (Var v, Ma)] nchotomy';
    6.50        in
    6.51          Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    6.52            (fn {context = ctxt, prems, ...} =>
     7.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Mar 05 13:28:04 2015 +0100
     7.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 00:00:57 2015 +0100
     7.3 @@ -89,24 +89,25 @@
     7.4        (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
     7.5      val Type (_, [_, iT]) = T;
     7.6      val icT = Thm.ctyp_of thy iT;
     7.7 -    val cert = Thm.cterm_of thy;
     7.8      val inst = Thm.instantiate_cterm ([(aT, icT)], []);
     7.9      fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
    7.10      val t_rhs = lambda t_k proto_t_rhs;
    7.11      val eqs0 = [subst_v @{term "0::natural"} eq,
    7.12        subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
    7.13      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
    7.14 -    val ((_, (_, eqs2)), lthy') = BNF_LFP_Compat.add_primrec_simple
    7.15 -      [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
    7.16 +    val ((_, (_, eqs2)), lthy') = lthy
    7.17 +      |> BNF_LFP_Compat.add_primrec_simple
    7.18 +        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
    7.19      val cT_random_aux = inst pt_random_aux;
    7.20      val cT_rhs = inst pt_rhs;
    7.21      val rule = @{thm random_aux_rec}
    7.22 -      |> Drule.instantiate_normalize ([(aT, icT)],
    7.23 -           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
    7.24 +      |> Drule.instantiate_normalize
    7.25 +        ([(aT, icT)],
    7.26 +          [(cT_random_aux, Thm.cterm_of thy t_random_aux), (cT_rhs, Thm.cterm_of thy t_rhs)]);
    7.27      fun tac ctxt =
    7.28        ALLGOALS (rtac rule)
    7.29        THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
    7.30 -      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
    7.31 +      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
    7.32      val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
    7.33    in (simp, lthy') end;
    7.34  
     8.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Thu Mar 05 13:28:04 2015 +0100
     8.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Mar 06 00:00:57 2015 +0100
     8.3 @@ -108,15 +108,13 @@
     8.4  
     8.5  fun match_instantiateT ctxt t thm =
     8.6    if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
     8.7 -    let val certT = Proof_Context.ctyp_of ctxt
     8.8 -    in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
     8.9 +    Thm.instantiate (gen_certify_inst fst TVar (Proof_Context.ctyp_of ctxt) ctxt thm t, []) thm
    8.10    else thm
    8.11  
    8.12  fun match_instantiate ctxt t thm =
    8.13 -  let
    8.14 -    val cert = Proof_Context.cterm_of ctxt
    8.15 -    val thm' = match_instantiateT ctxt t thm
    8.16 -  in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
    8.17 +  let val thm' = match_instantiateT ctxt t thm in
    8.18 +    Thm.instantiate ([], gen_certify_inst snd Var (Proof_Context.cterm_of ctxt) ctxt thm' t) thm'
    8.19 +  end
    8.20  
    8.21  fun apply_rule ctxt t =
    8.22    (case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
     9.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu Mar 05 13:28:04 2015 +0100
     9.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Mar 06 00:00:57 2015 +0100
     9.3 @@ -204,13 +204,13 @@
     9.4  
     9.5  fun certify_eval ctxt value conv ct =
     9.6    let
     9.7 -    val cert = Proof_Context.cterm_of ctxt;
     9.8      val t = Thm.term_of ct;
     9.9      val T = fastype_of t;
    9.10 -    val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
    9.11 +    val mk_eq =
    9.12 +      Thm.mk_binop (Proof_Context.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
    9.13    in case value ctxt t
    9.14     of NONE => Thm.reflexive ct
    9.15 -    | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
    9.16 +    | SOME t' => conv ctxt (mk_eq ct (Proof_Context.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
    9.17          handle THM _ =>
    9.18            error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
    9.19    end;
    10.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 05 13:28:04 2015 +0100
    10.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 00:00:57 2015 +0100
    10.3 @@ -27,7 +27,6 @@
    10.4  fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
    10.5    let
    10.6      val ctxt = Proof_Context.init_global thy;
    10.7 -    val cert = Thm.cterm_of thy;
    10.8  
    10.9      val recTs = Old_Datatype_Aux.get_rec_types descr;
   10.10      val pnames =
   10.11 @@ -106,11 +105,11 @@
   10.12          (map (fn ((((i, _), T), U), tname) =>
   10.13            make_pred i U T (mk_proj i is r) (Free (tname, T)))
   10.14              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   10.15 -    val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
   10.16 +    val inst = map (apply2 (Thm.cterm_of thy)) (map head_of (HOLogic.dest_conj
   10.17        (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
   10.18  
   10.19      val thm =
   10.20 -      Goal.prove_internal ctxt (map cert prems) (cert concl)
   10.21 +      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems) (Thm.cterm_of thy concl)
   10.22          (fn prems =>
   10.23             EVERY [
   10.24              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
   10.25 @@ -160,7 +159,6 @@
   10.26  fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
   10.27    let
   10.28      val ctxt = Proof_Context.init_global thy;
   10.29 -    val cert = Thm.cterm_of thy;
   10.30      val rT = TFree ("'P", @{sort type});
   10.31      val rT' = TVar (("'P", 0), @{sort type});
   10.32  
   10.33 @@ -187,11 +185,12 @@
   10.34      val y' = Free ("y", T);
   10.35  
   10.36      val thm =
   10.37 -      Goal.prove_internal ctxt (map cert prems)
   10.38 -        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
   10.39 +      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems)
   10.40 +        (Thm.cterm_of thy
   10.41 +          (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
   10.42          (fn prems =>
   10.43             EVERY [
   10.44 -            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
   10.45 +            rtac (cterm_instantiate [apply2 (Thm.cterm_of thy) (y, y')] exhaust) 1,
   10.46              ALLGOALS (EVERY'
   10.47                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
   10.48                 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
    11.1 --- a/src/HOL/Tools/record.ML	Thu Mar 05 13:28:04 2015 +0100
    11.2 +++ b/src/HOL/Tools/record.ML	Fri Mar 06 00:00:57 2015 +0100
    11.3 @@ -1460,8 +1460,6 @@
    11.4    avoid problems with higher order unification.*)
    11.5  fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
    11.6    let
    11.7 -    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
    11.8 -
    11.9      val g = Thm.term_of cgoal;
   11.10      val params = Logic.strip_params g;
   11.11      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
   11.12 @@ -1475,7 +1473,7 @@
   11.13        | [x] => (head_of x, false));
   11.14      val rule'' =
   11.15        cterm_instantiate
   11.16 -        (map (apply2 cert)
   11.17 +        (map (apply2 (Proof_Context.cterm_of ctxt))
   11.18            (case rev params of
   11.19              [] =>
   11.20                (case AList.lookup (op =) (Term.add_frees g []) s of
    12.1 --- a/src/HOL/Tools/reification.ML	Thu Mar 05 13:28:04 2015 +0100
    12.2 +++ b/src/HOL/Tools/reification.ML	Fri Mar 06 00:00:57 2015 +0100
    12.3 @@ -48,7 +48,6 @@
    12.4    let
    12.5      val Const (fN, _) = th |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
    12.6        |> fst |> strip_comb |> fst;
    12.7 -    val cert = Proof_Context.cterm_of ctxt;
    12.8      val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
    12.9      val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
   12.10      fun add_fterms (t as t1 $ t2) =
   12.11 @@ -84,7 +83,7 @@
   12.12          (fn {context, prems, ...} =>
   12.13            Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym;
   12.14      val (cong' :: vars') =
   12.15 -      Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs);
   12.16 +      Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Proof_Context.cterm_of ctxt'') vs);
   12.17      val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
   12.18  
   12.19    in (vs', cong') end;
   12.20 @@ -134,8 +133,6 @@
   12.21  fun decomp_reify da cgns (ct, ctxt) bds =
   12.22    let
   12.23      val thy = Proof_Context.theory_of ctxt;
   12.24 -    val cert = Thm.cterm_of thy;
   12.25 -    val certT = Thm.ctyp_of thy;
   12.26      fun tryabsdecomp (ct, ctxt) bds =
   12.27        (case Thm.term_of ct of
   12.28          Abs (_, xT, ta) =>
   12.29 @@ -143,8 +140,8 @@
   12.30              val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
   12.31              val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta);  (* FIXME !? *)
   12.32              val x = Free (xn, xT);
   12.33 -            val cx = cert x;
   12.34 -            val cta = cert ta;
   12.35 +            val cx = Proof_Context.cterm_of ctxt' x;
   12.36 +            val cta = Proof_Context.cterm_of ctxt' ta;
   12.37              val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
   12.38                  NONE => error "tryabsdecomp: Type not found in the Environement"
   12.39                | SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
   12.40 @@ -172,10 +169,12 @@
   12.41            val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
   12.42            val (fts, its) =
   12.43              (map (snd o snd) fnvs,
   12.44 -             map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t)) invs);
   12.45 -          val ctyenv = map (fn ((vn, vi), (s, ty)) => (certT (TVar((vn, vi), s)), certT ty)) (Vartab.dest tyenv);
   12.46 +             map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t)) invs);
   12.47 +          val ctyenv =
   12.48 +            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of thy) (TVar ((vn, vi), s), ty))
   12.49 +              (Vartab.dest tyenv);
   12.50          in
   12.51 -          ((map cert fts ~~ replicate (length fts) ctxt,
   12.52 +          ((map (Thm.cterm_of thy) fts ~~ replicate (length fts) ctxt,
   12.53               apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
   12.54          end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
   12.55    end;
   12.56 @@ -196,8 +195,6 @@
   12.57          val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt;
   12.58          val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt';
   12.59          val thy = Proof_Context.theory_of ctxt'';
   12.60 -        val cert = Thm.cterm_of thy;
   12.61 -        val certT = Thm.ctyp_of thy;
   12.62          val vsns_map = vss ~~ vsns;
   12.63          val xns_map = fst (split_list nths) ~~ xns;
   12.64          val subst = map (fn (nt, xn) => (nt, Var ((xn, 0), fastype_of nt))) xns_map;
   12.65 @@ -205,15 +202,15 @@
   12.66          val (tyenv, tmenv) = Pattern.match thy (rhs_P, Thm.term_of ct) (Vartab.empty, Vartab.empty);
   12.67          val sbst = Envir.subst_term (tyenv, tmenv);
   12.68          val sbsT = Envir.subst_type tyenv;
   12.69 -        val subst_ty = map (fn (n, (s, t)) =>
   12.70 -          (certT (TVar (n, s)), certT t)) (Vartab.dest tyenv)
   12.71 +        val subst_ty =
   12.72 +          map (fn (n, (s, t)) => apply2 (Thm.ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
   12.73          val tml = Vartab.dest tmenv;
   12.74          val (subst_ns, bds) = fold_map
   12.75            (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
   12.76              let
   12.77                val name = snd (the (AList.lookup (op =) tml xn0));
   12.78                val (idx, bds) = index_of name bds;
   12.79 -            in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds;
   12.80 +            in (apply2 (Thm.cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
   12.81          val subst_vs =
   12.82            let
   12.83              fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
   12.84 @@ -222,12 +219,13 @@
   12.85                  val lT' = sbsT lT;
   12.86                  val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
   12.87                  val vsn = the (AList.lookup (op =) vsns_map vs);
   12.88 -                val cvs = cert (fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT')));
   12.89 -              in (cert vs, cvs) end;
   12.90 +                val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
   12.91 +              in apply2 (Thm.cterm_of thy) (vs, vs') end;
   12.92            in map h subst end;
   12.93 -        val cts = map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t))
   12.94 -          (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
   12.95 -            (map (fn n => (n, 0)) xns) tml);
   12.96 +        val cts =
   12.97 +          map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t))
   12.98 +            (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
   12.99 +              (map (fn n => (n, 0)) xns) tml);
  12.100          val substt =
  12.101            let
  12.102              val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
  12.103 @@ -261,15 +259,17 @@
  12.104        |> fst)) eqs [];
  12.105      val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
  12.106      val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
  12.107 -    val cert = Proof_Context.cterm_of ctxt';
  12.108      val subst =
  12.109 -      the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs);
  12.110 +      the o AList.lookup (op =)
  12.111 +        (map2 (fn T => fn v => (T, Proof_Context.cterm_of ctxt' (Free (v, T)))) tys vs);
  12.112      fun prep_eq eq =
  12.113        let
  12.114          val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
  12.115            |> HOLogic.dest_eq |> fst |> strip_comb;
  12.116 -        val subst = map_filter (fn (v as Var (_, T)) => SOME (cert v, subst T)
  12.117 -          | _ => NONE) vs;
  12.118 +        val subst =
  12.119 +          map_filter
  12.120 +            (fn (v as Var (_, T)) => SOME (Proof_Context.cterm_of ctxt' v, subst T)
  12.121 +              | _ => NONE) vs;
  12.122        in Thm.instantiate ([], subst) eq end;
  12.123      val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
  12.124      val bds = AList.make (K ([], [])) tys;
  12.125 @@ -285,10 +285,9 @@
  12.126        | is_list_var _ = false;
  12.127      val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd
  12.128        |> strip_comb |> snd |> filter is_list_var;
  12.129 -    val cert = Proof_Context.cterm_of ctxt;
  12.130      val vs = map (fn v as Var (_, T) =>
  12.131        (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
  12.132 -    val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
  12.133 +    val th' = Drule.instantiate_normalize ([], map (apply2 (Proof_Context.cterm_of ctxt)) vs) th;
  12.134      val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
  12.135    in Thm.transitive th'' th' end;
  12.136