tuned -- more explicit use of context;
authorwenzelm
Thu Mar 05 13:28:04 2015 +0100 (2015-03-05)
changeset 59616eb59c6968219
parent 59593 304ee0a475d1
child 59617 b60e65ad13df
tuned -- more explicit use of context;
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Tools/rule_insts.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/more_thm.ML
src/Pure/subgoal.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/element.ML	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Mar 05 13:28:04 2015 +0100
     1.3 @@ -201,9 +201,9 @@
     1.4    (case Object_Logic.elim_concl th of
     1.5      SOME C =>
     1.6        let
     1.7 -        val cert = Thm.cterm_of (Thm.theory_of_thm th);
     1.8 +        val thy = Thm.theory_of_thm th;
     1.9          val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
    1.10 -        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
    1.11 +        val th' = Thm.instantiate ([], [(Thm.cterm_of thy C, Thm.cterm_of thy thesis)]) th;
    1.12        in (th', true) end
    1.13    | NONE => (th, false));
    1.14  
    1.15 @@ -338,9 +338,8 @@
    1.16  
    1.17  fun instantiate_tfrees thy subst th =
    1.18    let
    1.19 -    val certT = Thm.ctyp_of thy;
    1.20      val idx = Thm.maxidx_of th + 1;
    1.21 -    fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
    1.22 +    fun cert_inst (a, (S, T)) = (Thm.ctyp_of thy (TVar ((a, idx), S)), Thm.ctyp_of thy T);
    1.23  
    1.24      fun add_inst (a, S) insts =
    1.25        if AList.defined (op =) insts a then insts
    1.26 @@ -355,10 +354,8 @@
    1.27    end;
    1.28  
    1.29  fun instantiate_frees thy subst =
    1.30 -  let val cert = Thm.cterm_of thy in
    1.31 -    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
    1.32 -    Drule.forall_elim_list (map (cert o snd) subst)
    1.33 -  end;
    1.34 +  Drule.forall_intr_list (map (Thm.cterm_of thy o Free o fst) subst) #>
    1.35 +  Drule.forall_elim_list (map (Thm.cterm_of thy o snd) subst);
    1.36  
    1.37  fun hyps_rule rule th =
    1.38    let val {hyps, ...} = Thm.crep_thm th in
     2.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 05 11:11:42 2015 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Thu Mar 05 13:28:04 2015 +0100
     2.3 @@ -678,18 +678,17 @@
     2.4          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
     2.5      val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
     2.6  
     2.7 -    val cert = Thm.cterm_of defs_thy;
     2.8 -
     2.9      val intro = Goal.prove_global defs_thy [] norm_ts statement
    2.10        (fn {context = ctxt, ...} =>
    2.11          rewrite_goals_tac ctxt [pred_def] THEN
    2.12          compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    2.13          compose_tac defs_ctxt
    2.14 -          (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    2.15 +          (false,
    2.16 +            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1);
    2.17  
    2.18      val conjuncts =
    2.19        (Drule.equal_elim_rule2 OF
    2.20 -        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
    2.21 +        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))])
    2.22        |> Conjunction.elim_balanced (length ts);
    2.23  
    2.24      val (_, axioms_ctxt) = defs_ctxt
     3.1 --- a/src/Pure/Isar/generic_target.ML	Thu Mar 05 11:11:42 2015 +0100
     3.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Mar 05 13:28:04 2015 +0100
     3.3 @@ -176,11 +176,10 @@
     3.4  
     3.5  fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
     3.6    let
     3.7 -    val thy = Proof_Context.theory_of lthy;
     3.8 -    val thy_ctxt = Proof_Context.init_global thy;
     3.9 +    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
    3.10  
    3.11      (*term and type parameters*)
    3.12 -    val ((defs, _), rhs') = Thm.cterm_of thy rhs
    3.13 +    val ((defs, _), rhs') = Proof_Context.cterm_of lthy rhs
    3.14        |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
    3.15  
    3.16      val xs = Variable.add_fixed lthy rhs' [];
    3.17 @@ -218,10 +217,7 @@
    3.18  
    3.19  fun import_export_proof ctxt (name, raw_th) =
    3.20    let
    3.21 -    val thy = Proof_Context.theory_of ctxt;
    3.22 -    val thy_ctxt = Proof_Context.init_global thy;
    3.23 -    val certT = Thm.ctyp_of thy;
    3.24 -    val cert = Thm.cterm_of thy;
    3.25 +    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt);
    3.26  
    3.27      (*export assumes/defines*)
    3.28      val th = Goal.norm_result ctxt raw_th;
    3.29 @@ -232,7 +228,7 @@
    3.30      val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
    3.31      val frees = map Free (Thm.fold_terms Term.add_frees th' []);
    3.32      val (th'' :: vs) =
    3.33 -      (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
    3.34 +      (th' :: map (Drule.mk_term o Proof_Context.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
    3.35        |> Variable.export ctxt thy_ctxt
    3.36        |> Drule.zero_var_indexes_list;
    3.37  
    3.38 @@ -246,8 +242,10 @@
    3.39  
    3.40      val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
    3.41      val inst = filter (is_Var o fst) (vars ~~ frees);
    3.42 -    val cinstT = map (apply2 certT o apfst TVar) instT;
    3.43 -    val cinst = map (apply2 (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
    3.44 +    val cinstT = instT
    3.45 +      |> map (apply2 (Proof_Context.ctyp_of ctxt) o apfst TVar);
    3.46 +    val cinst = inst
    3.47 +      |> map (apply2 (Proof_Context.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
    3.48      val result' = Thm.instantiate (cinstT, cinst) result;
    3.49  
    3.50      (*import assumes/defines*)
     4.1 --- a/src/Pure/Isar/obtain.ML	Thu Mar 05 11:11:42 2015 +0100
     4.2 +++ b/src/Pure/Isar/obtain.ML	Thu Mar 05 13:28:04 2015 +0100
     4.3 @@ -112,8 +112,6 @@
     4.4      name raw_vars raw_asms int state =
     4.5    let
     4.6      val _ = Proof.assert_forward_or_chain state;
     4.7 -    val thy = Proof.theory_of state;
     4.8 -    val cert = Thm.cterm_of thy;
     4.9      val ctxt = Proof.context_of state;
    4.10      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    4.11  
    4.12 @@ -131,6 +129,7 @@
    4.13      (*obtain parms*)
    4.14      val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
    4.15      val parms = map Free (xs' ~~ Ts);
    4.16 +    val cparms = map (Proof_Context.cterm_of ctxt) parms;
    4.17      val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
    4.18  
    4.19      (*obtain statements*)
    4.20 @@ -149,7 +148,7 @@
    4.21        Proof.local_qed (NONE, false)
    4.22        #> `Proof.the_fact #-> (fn rule =>
    4.23          Proof.fix vars
    4.24 -        #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms);
    4.25 +        #> Proof.assm (obtain_export fix_ctxt rule cparms) asms);
    4.26    in
    4.27      state
    4.28      |> Proof.enter_forward
    4.29 @@ -187,18 +186,18 @@
    4.30  
    4.31  fun result tac facts ctxt =
    4.32    let
    4.33 -    val cert = Proof_Context.cterm_of ctxt;
    4.34 -
    4.35      val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
    4.36 +    val st = Goal.init (Proof_Context.cterm_of ctxt thesis);
    4.37      val rule =
    4.38 -      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
    4.39 +      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
    4.40          NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
    4.41        | SOME th =>
    4.42            check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
    4.43  
    4.44 -    val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
    4.45 +    val closed_rule = Thm.forall_intr (Proof_Context.cterm_of ctxt (Free thesis_var)) rule;
    4.46      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
    4.47 -    val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
    4.48 +    val obtain_rule =
    4.49 +      Thm.forall_elim (Proof_Context.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule';
    4.50      val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
    4.51      val (prems, ctxt'') =
    4.52        Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
    4.53 @@ -214,8 +213,6 @@
    4.54  fun unify_params vars thesis_var raw_rule ctxt =
    4.55    let
    4.56      val thy = Proof_Context.theory_of ctxt;
    4.57 -    val certT = Thm.ctyp_of thy;
    4.58 -    val cert = Thm.cterm_of thy;
    4.59      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    4.60  
    4.61      fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
    4.62 @@ -240,20 +237,20 @@
    4.63      val xs = map (apsnd norm_type o fst) vars;
    4.64      val ys = map (apsnd norm_type) (drop m params);
    4.65      val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
    4.66 -    val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
    4.67 +    val terms = map (Drule.mk_term o Thm.cterm_of thy o Free) (xs @ ys');
    4.68  
    4.69      val instT =
    4.70        fold (Term.add_tvarsT o #2) params []
    4.71 -      |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
    4.72 +      |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
    4.73      val closed_rule = rule
    4.74 -      |> Thm.forall_intr (cert (Free thesis_var))
    4.75 +      |> Thm.forall_intr (Thm.cterm_of thy (Free thesis_var))
    4.76        |> Thm.instantiate (instT, []);
    4.77  
    4.78      val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
    4.79      val vars' =
    4.80        map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
    4.81        (map snd vars @ replicate (length ys) NoSyn);
    4.82 -    val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
    4.83 +    val rule'' = Thm.forall_elim (Thm.cterm_of thy (Logic.varify_global (Free thesis_var))) rule';
    4.84    in ((vars', rule''), ctxt') end;
    4.85  
    4.86  fun inferred_type (binding, _, mx) ctxt =
    4.87 @@ -270,7 +267,6 @@
    4.88    let
    4.89      val _ = Proof.assert_forward_or_chain state;
    4.90      val ctxt = Proof.context_of state;
    4.91 -    val cert = Proof_Context.cterm_of ctxt;
    4.92      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    4.93  
    4.94      val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
    4.95 @@ -292,7 +288,8 @@
    4.96          |> Proof.map_context (K ctxt')
    4.97          |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
    4.98          |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
    4.99 -          (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
   4.100 +          (obtain_export fix_ctxt rule (map (Proof_Context.cterm_of ctxt) ts))
   4.101 +            [(Thm.empty_binding, asms)])
   4.102          |> Proof.bind_terms Auto_Bind.no_facts
   4.103        end;
   4.104  
   4.105 @@ -314,7 +311,8 @@
   4.106      |> Proof.chain_facts chain_facts
   4.107      |> Proof.local_goal print_result (K I) (pair o rpair I)
   4.108        "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
   4.109 -    |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (cert thesis))) |> Seq.hd
   4.110 +    |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
   4.111 +        Goal.init (Proof_Context.cterm_of ctxt thesis))) |> Seq.hd
   4.112    end;
   4.113  
   4.114  in
     5.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 05 11:11:42 2015 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 05 13:28:04 2015 +0100
     5.3 @@ -894,7 +894,6 @@
     5.4  fun generic_goal prepp kind before_qed after_qed raw_propp state =
     5.5    let
     5.6      val ctxt = context_of state;
     5.7 -    val cert = Proof_Context.cterm_of ctxt;
     5.8      val chaining = can assert_chain state;
     5.9      val pos = Position.thread_data ();
    5.10  
    5.11 @@ -910,7 +909,8 @@
    5.12      val propss' = vars :: propss;
    5.13      val goal_propss = filter_out null propss';
    5.14      val goal =
    5.15 -      cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
    5.16 +      Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
    5.17 +      |> Proof_Context.cterm_of ctxt
    5.18        |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
    5.19      val statement = ((kind, pos), propss', Thm.term_of goal);
    5.20      val after_qed' = after_qed |>> (fn after_local =>
     6.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 05 11:11:42 2015 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 05 13:28:04 2015 +0100
     6.3 @@ -1166,10 +1166,10 @@
     6.4  
     6.5  fun gen_assms prepp exp args ctxt =
     6.6    let
     6.7 -    val cert = cterm_of ctxt;
     6.8      val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
     6.9      val _ = Variable.warn_extra_tfrees ctxt ctxt1;
    6.10 -    val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
    6.11 +    val (premss, ctxt2) =
    6.12 +      fold_burrow (Assumption.add_assms exp o map (cterm_of ctxt)) propss ctxt1;
    6.13    in
    6.14      ctxt2
    6.15      |> auto_bind_facts (flat propss)
     7.1 --- a/src/Pure/Tools/rule_insts.ML	Thu Mar 05 11:11:42 2015 +0100
     7.2 +++ b/src/Pure/Tools/rule_insts.ML	Thu Mar 05 13:28:04 2015 +0100
     7.3 @@ -81,8 +81,6 @@
     7.4  fun read_insts ctxt mixed_insts (tvars, vars) =
     7.5    let
     7.6      val thy = Proof_Context.theory_of ctxt;
     7.7 -    val cert = Thm.cterm_of thy;
     7.8 -    val certT = Thm.ctyp_of thy;
     7.9  
    7.10      val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
    7.11  
    7.12 @@ -118,7 +116,8 @@
    7.13      val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
    7.14      val inst_vars = map_filter (make_inst inst2) vars2;
    7.15    in
    7.16 -    (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars)
    7.17 +    (map (apply2 (Thm.ctyp_of thy)) inst_tvars,
    7.18 +     map (apply2 (Thm.cterm_of thy)) inst_vars)
    7.19    end;
    7.20  
    7.21  fun where_rule ctxt mixed_insts fixes thm =
    7.22 @@ -282,9 +281,9 @@
    7.23  
    7.24  fun make_elim_preserve ctxt rl =
    7.25    let
    7.26 -    val cert = Thm.cterm_of (Thm.theory_of_thm rl);
    7.27 +    val thy = Thm.theory_of_thm rl;
    7.28      val maxidx = Thm.maxidx_of rl;
    7.29 -    fun cvar xi = cert (Var (xi, propT));
    7.30 +    fun cvar xi = Thm.cterm_of thy (Var (xi, propT));
    7.31      val revcut_rl' =
    7.32        Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
    7.33          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
     8.1 --- a/src/Pure/drule.ML	Thu Mar 05 11:11:42 2015 +0100
     8.2 +++ b/src/Pure/drule.ML	Thu Mar 05 13:28:04 2015 +0100
     8.3 @@ -210,10 +210,8 @@
     8.4  (*generalize outermost parameters*)
     8.5  fun gen_all th =
     8.6    let
     8.7 -    val thy = Thm.theory_of_thm th;
     8.8 -    val {prop, maxidx, ...} = Thm.rep_thm th;
     8.9 -    val cert = Thm.cterm_of thy;
    8.10 -    fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T)));
    8.11 +    val {thy, prop, maxidx, ...} = Thm.rep_thm th;
    8.12 +    fun elim (x, T) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T)));
    8.13    in fold elim (outer_params prop) th end;
    8.14  
    8.15  (*lift vars wrt. outermost goal parameters
    8.16 @@ -221,16 +219,15 @@
    8.17  fun lift_all goal th =
    8.18    let
    8.19      val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
    8.20 -    val cert = Thm.cterm_of thy;
    8.21      val maxidx = Thm.maxidx_of th;
    8.22      val ps = outer_params (Thm.term_of goal)
    8.23        |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
    8.24      val Ts = map Term.fastype_of ps;
    8.25      val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) =>
    8.26 -      (cert (Var (xi, T)), cert (Term.list_comb (Var (xi, Ts ---> T), ps))));
    8.27 +      (Thm.cterm_of thy (Var (xi, T)), Thm.cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps))));
    8.28    in
    8.29      th |> Thm.instantiate ([], inst)
    8.30 -    |> fold_rev (Thm.forall_intr o cert) ps
    8.31 +    |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) ps
    8.32    end;
    8.33  
    8.34  (*direct generalization*)
    8.35 @@ -250,10 +247,9 @@
    8.36    | zero_var_indexes_list ths =
    8.37        let
    8.38          val thy = Theory.merge_list (map Thm.theory_of_thm ths);
    8.39 -        val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
    8.40          val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
    8.41 -        val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    8.42 -        val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    8.43 +        val cinstT = map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT;
    8.44 +        val cinst = map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst;
    8.45        in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
    8.46  
    8.47  val zero_var_indexes = singleton zero_var_indexes_list;
    8.48 @@ -647,12 +643,10 @@
    8.49  fun mk_term ct =
    8.50    let
    8.51      val thy = Thm.theory_of_cterm ct;
    8.52 -    val cert = Thm.cterm_of thy;
    8.53 -    val certT = Thm.ctyp_of thy;
    8.54      val T = Thm.typ_of_cterm ct;
    8.55 -    val a = certT (TVar (("'a", 0), []));
    8.56 -    val x = cert (Var (("x", 0), T));
    8.57 -  in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
    8.58 +    val a = Thm.ctyp_of thy (TVar (("'a", 0), []));
    8.59 +    val x = Thm.cterm_of thy (Var (("x", 0), T));
    8.60 +  in Thm.instantiate ([(a, Thm.ctyp_of thy T)], [(x, ct)]) termI end;
    8.61  
    8.62  fun dest_term th =
    8.63    let val cprop = strip_imp_concl (Thm.cprop_of th) in
    8.64 @@ -793,10 +787,9 @@
    8.65    | cterm_instantiate ctpairs th =
    8.66        let
    8.67          val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
    8.68 -        val certT = Thm.ctyp_of thy;
    8.69          val instT =
    8.70            Vartab.fold (fn (xi, (S, T)) =>
    8.71 -            cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye [];
    8.72 +            cons (Thm.ctyp_of thy (TVar (xi, S)), Thm.ctyp_of thy (Envir.norm_type tye T))) tye [];
    8.73          val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
    8.74        in instantiate_normalize (instT, inst) th end
    8.75        handle TERM (msg, _) => raise THM (msg, 0, [th])
    8.76 @@ -846,18 +839,18 @@
    8.77  fun rename_bvars [] thm = thm
    8.78    | rename_bvars vs thm =
    8.79        let
    8.80 -        val cert = Thm.cterm_of (Thm.theory_of_thm thm);
    8.81 +        val thy = Thm.theory_of_thm thm;
    8.82          fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
    8.83            | ren (t $ u) = ren t $ ren u
    8.84            | ren t = t;
    8.85 -      in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end;
    8.86 +      in Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy (ren (Thm.prop_of thm)))) thm end;
    8.87  
    8.88  
    8.89  (* renaming in left-to-right order *)
    8.90  
    8.91  fun rename_bvars' xs thm =
    8.92    let
    8.93 -    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
    8.94 +    val thy = Thm.theory_of_thm thm;
    8.95      val prop = Thm.prop_of thm;
    8.96      fun rename [] t = ([], t)
    8.97        | rename (x' :: xs) (Abs (x, T, t)) =
    8.98 @@ -869,9 +862,10 @@
    8.99              val (xs'', u') = rename xs' u
   8.100            in (xs'', t' $ u') end
   8.101        | rename xs t = (xs, t);
   8.102 -  in case rename xs prop of
   8.103 -      ([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm
   8.104 -    | _ => error "More names than abstractions in theorem"
   8.105 +  in
   8.106 +    (case rename xs prop of
   8.107 +      ([], prop') => Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy prop')) thm
   8.108 +    | _ => error "More names than abstractions in theorem")
   8.109    end;
   8.110  
   8.111  end;
     9.1 --- a/src/Pure/goal.ML	Thu Mar 05 11:11:42 2015 +0100
     9.2 +++ b/src/Pure/goal.ML	Thu Mar 05 13:28:04 2015 +0100
     9.3 @@ -128,20 +128,20 @@
     9.4  fun future_result ctxt result prop =
     9.5    let
     9.6      val thy = Proof_Context.theory_of ctxt;
     9.7 -    val cert = Thm.cterm_of thy;
     9.8 -    val certT = Thm.ctyp_of thy;
     9.9  
    9.10      val assms = Assumption.all_assms_of ctxt;
    9.11      val As = map Thm.term_of assms;
    9.12  
    9.13      val xs = map Free (fold Term.add_frees (prop :: As) []);
    9.14 -    val fixes = map cert xs;
    9.15 +    val fixes = map (Thm.cterm_of thy) xs;
    9.16  
    9.17      val tfrees = fold Term.add_tfrees (prop :: As) [];
    9.18 -    val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
    9.19 +    val instT =
    9.20 +      map (fn (a, S) => (Thm.ctyp_of thy (TVar ((a, 0), S)), Thm.ctyp_of thy (TFree (a, S)))) tfrees;
    9.21  
    9.22      val global_prop =
    9.23 -      cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
    9.24 +      Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
    9.25 +      |> Thm.cterm_of thy
    9.26        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
    9.27      val global_result = result |> Future.map
    9.28        (Drule.flexflex_unique (SOME ctxt) #>
    10.1 --- a/src/Pure/more_thm.ML	Thu Mar 05 11:11:42 2015 +0100
    10.2 +++ b/src/Pure/more_thm.ML	Thu Mar 05 13:28:04 2015 +0100
    10.3 @@ -116,18 +116,21 @@
    10.4  
    10.5  fun add_cterm_frees ct =
    10.6    let
    10.7 -    val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
    10.8 +    val thy = Thm.theory_of_cterm ct;
    10.9      val t = Thm.term_of ct;
   10.10 -  in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end;
   10.11 +  in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.cterm_of thy v) | _ => I) t end;
   10.12  
   10.13  
   10.14  (* cterm constructors and destructors *)
   10.15  
   10.16  fun all_name (x, t) A =
   10.17    let
   10.18 -    val cert = Thm.cterm_of (Thm.theory_of_cterm t);
   10.19 +    val thy = Thm.theory_of_cterm t;
   10.20      val T = Thm.typ_of_cterm t;
   10.21 -  in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
   10.22 +  in
   10.23 +    Thm.apply (Thm.cterm_of thy (Const ("Pure.all", (T --> propT) --> propT)))
   10.24 +      (Thm.lambda_name (x, t) A)
   10.25 +  end;
   10.26  
   10.27  fun all t A = all_name ("", t) A;
   10.28  
    11.1 --- a/src/Pure/subgoal.ML	Thu Mar 05 11:11:42 2015 +0100
    11.2 +++ b/src/Pure/subgoal.ML	Thu Mar 05 13:28:04 2015 +0100
    11.3 @@ -67,7 +67,6 @@
    11.4  *)
    11.5  fun lift_import idx params th ctxt =
    11.6    let
    11.7 -    val cert = Proof_Context.cterm_of ctxt;
    11.8      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    11.9  
   11.10      val Ts = map Thm.typ_of_cterm params;
   11.11 @@ -86,7 +85,8 @@
   11.12            else (Ts ---> T, ts);
   11.13          val u = Free (y, U);
   11.14          in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
   11.15 -    val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys));
   11.16 +    val (inst1, inst2) =
   11.17 +      split_list (map (apply2 (apply2 (Proof_Context.cterm_of ctxt))) (map2 var_inst vars ys));
   11.18  
   11.19      val th'' = Thm.instantiate ([], inst1) th';
   11.20    in ((inst2, th''), ctxt'') end;
    12.1 --- a/src/Pure/variable.ML	Thu Mar 05 11:11:42 2015 +0100
    12.2 +++ b/src/Pure/variable.ML	Thu Mar 05 13:28:04 2015 +0100
    12.3 @@ -587,9 +587,9 @@
    12.4  
    12.5  fun focus_cterm goal ctxt =
    12.6    let
    12.7 -    val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
    12.8 +    val thy = Thm.theory_of_cterm goal;
    12.9      val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
   12.10 -    val ps' = map (cert o Free) ps;
   12.11 +    val ps' = map (Thm.cterm_of thy o Free) ps;
   12.12      val goal' = fold forall_elim_prop ps' goal;
   12.13    in ((xs ~~ ps', goal'), ctxt') end;
   12.14