tuned -- more explicit use of context;

--- a/src/Pure/Isar/element.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/element.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -201,9 +201,9 @@
   (case Object_Logic.elim_concl th of
     SOME C =>
       let
-        val cert = Thm.cterm_of (Thm.theory_of_thm th);
+        val thy = Thm.theory_of_thm th;
         val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
-        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
+        val th' = Thm.instantiate ([], [(Thm.cterm_of thy C, Thm.cterm_of thy thesis)]) th;
       in (th', true) end
   | NONE => (th, false));
 
@@ -338,9 +338,8 @@
 
 fun instantiate_tfrees thy subst th =
   let
-    val certT = Thm.ctyp_of thy;
     val idx = Thm.maxidx_of th + 1;
-    fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
+    fun cert_inst (a, (S, T)) = (Thm.ctyp_of thy (TVar ((a, idx), S)), Thm.ctyp_of thy T);
 
     fun add_inst (a, S) insts =
       if AList.defined (op =) insts a then insts
@@ -355,10 +354,8 @@
   end;
 
 fun instantiate_frees thy subst =
-  let val cert = Thm.cterm_of thy in
-    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
-    Drule.forall_elim_list (map (cert o snd) subst)
-  end;
+  Drule.forall_intr_list (map (Thm.cterm_of thy o Free o fst) subst) #>
+  Drule.forall_elim_list (map (Thm.cterm_of thy o snd) subst);
 
 fun hyps_rule rule th =
   let val {hyps, ...} = Thm.crep_thm th in

--- a/src/Pure/Isar/expression.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -678,18 +678,17 @@
         [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
     val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
 
-    val cert = Thm.cterm_of defs_thy;
-
     val intro = Goal.prove_global defs_thy [] norm_ts statement
       (fn {context = ctxt, ...} =>
         rewrite_goals_tac ctxt [pred_def] THEN
         compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
         compose_tac defs_ctxt
-          (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+          (false,
+            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF
-        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
+        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))])
       |> Conjunction.elim_balanced (length ts);
 
     val (_, axioms_ctxt) = defs_ctxt

--- a/src/Pure/Isar/generic_target.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/generic_target.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -176,11 +176,10 @@
 
 fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
   let
-    val thy = Proof_Context.theory_of lthy;
-    val thy_ctxt = Proof_Context.init_global thy;
+    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
     (*term and type parameters*)
-    val ((defs, _), rhs') = Thm.cterm_of thy rhs
+    val ((defs, _), rhs') = Proof_Context.cterm_of lthy rhs
       |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
 
     val xs = Variable.add_fixed lthy rhs' [];
@@ -218,10 +217,7 @@
 
 fun import_export_proof ctxt (name, raw_th) =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val thy_ctxt = Proof_Context.init_global thy;
-    val certT = Thm.ctyp_of thy;
-    val cert = Thm.cterm_of thy;
+    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt);
 
     (*export assumes/defines*)
     val th = Goal.norm_result ctxt raw_th;
@@ -232,7 +228,7 @@
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
     val frees = map Free (Thm.fold_terms Term.add_frees th' []);
     val (th'' :: vs) =
-      (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
+      (th' :: map (Drule.mk_term o Proof_Context.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
       |> Drule.zero_var_indexes_list;
 
@@ -246,8 +242,10 @@
 
     val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
     val inst = filter (is_Var o fst) (vars ~~ frees);
-    val cinstT = map (apply2 certT o apfst TVar) instT;
-    val cinst = map (apply2 (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
+    val cinstT = instT
+      |> map (apply2 (Proof_Context.ctyp_of ctxt) o apfst TVar);
+    val cinst = inst
+      |> map (apply2 (Proof_Context.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
     val result' = Thm.instantiate (cinstT, cinst) result;
 
     (*import assumes/defines*)

--- a/src/Pure/Isar/obtain.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -112,8 +112,6 @@
     name raw_vars raw_asms int state =
   let
     val _ = Proof.assert_forward_or_chain state;
-    val thy = Proof.theory_of state;
-    val cert = Thm.cterm_of thy;
     val ctxt = Proof.context_of state;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
@@ -131,6 +129,7 @@
     (*obtain parms*)
     val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
     val parms = map Free (xs' ~~ Ts);
+    val cparms = map (Proof_Context.cterm_of ctxt) parms;
     val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
 
     (*obtain statements*)
@@ -149,7 +148,7 @@
       Proof.local_qed (NONE, false)
       #> `Proof.the_fact #-> (fn rule =>
         Proof.fix vars
-        #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms);
+        #> Proof.assm (obtain_export fix_ctxt rule cparms) asms);
   in
     state
     |> Proof.enter_forward
@@ -187,18 +186,18 @@
 
 fun result tac facts ctxt =
   let
-    val cert = Proof_Context.cterm_of ctxt;
-
     val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
+    val st = Goal.init (Proof_Context.cterm_of ctxt thesis);
     val rule =
-      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
+      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
       | SOME th =>
           check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
 
-    val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
+    val closed_rule = Thm.forall_intr (Proof_Context.cterm_of ctxt (Free thesis_var)) rule;
     val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
-    val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
+    val obtain_rule =
+      Thm.forall_elim (Proof_Context.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule';
     val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
       Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
@@ -214,8 +213,6 @@
 fun unify_params vars thesis_var raw_rule ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val certT = Thm.ctyp_of thy;
-    val cert = Thm.cterm_of thy;
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
@@ -240,20 +237,20 @@
     val xs = map (apsnd norm_type o fst) vars;
     val ys = map (apsnd norm_type) (drop m params);
     val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
-    val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
+    val terms = map (Drule.mk_term o Thm.cterm_of thy o Free) (xs @ ys');
 
     val instT =
       fold (Term.add_tvarsT o #2) params []
-      |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
+      |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
     val closed_rule = rule
-      |> Thm.forall_intr (cert (Free thesis_var))
+      |> Thm.forall_intr (Thm.cterm_of thy (Free thesis_var))
       |> Thm.instantiate (instT, []);
 
     val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
     val vars' =
       map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
       (map snd vars @ replicate (length ys) NoSyn);
-    val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
+    val rule'' = Thm.forall_elim (Thm.cterm_of thy (Logic.varify_global (Free thesis_var))) rule';
   in ((vars', rule''), ctxt') end;
 
 fun inferred_type (binding, _, mx) ctxt =
@@ -270,7 +267,6 @@
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
-    val cert = Proof_Context.cterm_of ctxt;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
@@ -292,7 +288,8 @@
         |> Proof.map_context (K ctxt')
         |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
-          (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
+          (obtain_export fix_ctxt rule (map (Proof_Context.cterm_of ctxt) ts))
+            [(Thm.empty_binding, asms)])
         |> Proof.bind_terms Auto_Bind.no_facts
       end;
 
@@ -314,7 +311,8 @@
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (pair o rpair I)
       "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
-    |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (cert thesis))) |> Seq.hd
+    |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
+        Goal.init (Proof_Context.cterm_of ctxt thesis))) |> Seq.hd
   end;
 
 in

--- a/src/Pure/Isar/proof.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -894,7 +894,6 @@
 fun generic_goal prepp kind before_qed after_qed raw_propp state =
   let
     val ctxt = context_of state;
-    val cert = Proof_Context.cterm_of ctxt;
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
@@ -910,7 +909,8 @@
     val propss' = vars :: propss;
     val goal_propss = filter_out null propss';
     val goal =
-      cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
+      Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
+      |> Proof_Context.cterm_of ctxt
       |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
     val statement = ((kind, pos), propss', Thm.term_of goal);
     val after_qed' = after_qed |>> (fn after_local =>

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -1166,10 +1166,10 @@
 
 fun gen_assms prepp exp args ctxt =
   let
-    val cert = cterm_of ctxt;
     val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
     val _ = Variable.warn_extra_tfrees ctxt ctxt1;
-    val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
+    val (premss, ctxt2) =
+      fold_burrow (Assumption.add_assms exp o map (cterm_of ctxt)) propss ctxt1;
   in
     ctxt2
     |> auto_bind_facts (flat propss)

--- a/src/Pure/Tools/rule_insts.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -81,8 +81,6 @@
 fun read_insts ctxt mixed_insts (tvars, vars) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
 
     val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
 
@@ -118,7 +116,8 @@
     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
     val inst_vars = map_filter (make_inst inst2) vars2;
   in
-    (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars)
+    (map (apply2 (Thm.ctyp_of thy)) inst_tvars,
+     map (apply2 (Thm.cterm_of thy)) inst_vars)
   end;
 
 fun where_rule ctxt mixed_insts fixes thm =
@@ -282,9 +281,9 @@
 
 fun make_elim_preserve ctxt rl =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm rl);
+    val thy = Thm.theory_of_thm rl;
     val maxidx = Thm.maxidx_of rl;
-    fun cvar xi = cert (Var (xi, propT));
+    fun cvar xi = Thm.cterm_of thy (Var (xi, propT));
     val revcut_rl' =
       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;

--- a/src/Pure/drule.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/drule.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -210,10 +210,8 @@
 (*generalize outermost parameters*)
 fun gen_all th =
   let
-    val thy = Thm.theory_of_thm th;
-    val {prop, maxidx, ...} = Thm.rep_thm th;
-    val cert = Thm.cterm_of thy;
-    fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T)));
+    val {thy, prop, maxidx, ...} = Thm.rep_thm th;
+    fun elim (x, T) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T)));
   in fold elim (outer_params prop) th end;
 
 (*lift vars wrt. outermost goal parameters
@@ -221,16 +219,15 @@
 fun lift_all goal th =
   let
     val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
-    val cert = Thm.cterm_of thy;
     val maxidx = Thm.maxidx_of th;
     val ps = outer_params (Thm.term_of goal)
       |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
     val Ts = map Term.fastype_of ps;
     val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) =>
-      (cert (Var (xi, T)), cert (Term.list_comb (Var (xi, Ts ---> T), ps))));
+      (Thm.cterm_of thy (Var (xi, T)), Thm.cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps))));
   in
     th |> Thm.instantiate ([], inst)
-    |> fold_rev (Thm.forall_intr o cert) ps
+    |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) ps
   end;
 
 (*direct generalization*)
@@ -250,10 +247,9 @@
   | zero_var_indexes_list ths =
       let
         val thy = Theory.merge_list (map Thm.theory_of_thm ths);
-        val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
         val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
-        val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
-        val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
+        val cinstT = map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT;
+        val cinst = map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst;
       in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
@@ -647,12 +643,10 @@
 fun mk_term ct =
   let
     val thy = Thm.theory_of_cterm ct;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
     val T = Thm.typ_of_cterm ct;
-    val a = certT (TVar (("'a", 0), []));
-    val x = cert (Var (("x", 0), T));
-  in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
+    val a = Thm.ctyp_of thy (TVar (("'a", 0), []));
+    val x = Thm.cterm_of thy (Var (("x", 0), T));
+  in Thm.instantiate ([(a, Thm.ctyp_of thy T)], [(x, ct)]) termI end;
 
 fun dest_term th =
   let val cprop = strip_imp_concl (Thm.cprop_of th) in
@@ -793,10 +787,9 @@
   | cterm_instantiate ctpairs th =
       let
         val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
-        val certT = Thm.ctyp_of thy;
         val instT =
           Vartab.fold (fn (xi, (S, T)) =>
-            cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye [];
+            cons (Thm.ctyp_of thy (TVar (xi, S)), Thm.ctyp_of thy (Envir.norm_type tye T))) tye [];
         val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
       in instantiate_normalize (instT, inst) th end
       handle TERM (msg, _) => raise THM (msg, 0, [th])
@@ -846,18 +839,18 @@
 fun rename_bvars [] thm = thm
   | rename_bvars vs thm =
       let
-        val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+        val thy = Thm.theory_of_thm thm;
         fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
           | ren (t $ u) = ren t $ ren u
           | ren t = t;
-      in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end;
+      in Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy (ren (Thm.prop_of thm)))) thm end;
 
 
 (* renaming in left-to-right order *)
 
 fun rename_bvars' xs thm =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+    val thy = Thm.theory_of_thm thm;
     val prop = Thm.prop_of thm;
     fun rename [] t = ([], t)
       | rename (x' :: xs) (Abs (x, T, t)) =
@@ -869,9 +862,10 @@
             val (xs'', u') = rename xs' u
           in (xs'', t' $ u') end
       | rename xs t = (xs, t);
-  in case rename xs prop of
-      ([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm
-    | _ => error "More names than abstractions in theorem"
+  in
+    (case rename xs prop of
+      ([], prop') => Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy prop')) thm
+    | _ => error "More names than abstractions in theorem")
   end;
 
 end;

--- a/src/Pure/goal.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/goal.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -128,20 +128,20 @@
 fun future_result ctxt result prop =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
 
     val assms = Assumption.all_assms_of ctxt;
     val As = map Thm.term_of assms;
 
     val xs = map Free (fold Term.add_frees (prop :: As) []);
-    val fixes = map cert xs;
+    val fixes = map (Thm.cterm_of thy) xs;
 
     val tfrees = fold Term.add_tfrees (prop :: As) [];
-    val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
+    val instT =
+      map (fn (a, S) => (Thm.ctyp_of thy (TVar ((a, 0), S)), Thm.ctyp_of thy (TFree (a, S)))) tfrees;
 
     val global_prop =
-      cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+      Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
+      |> Thm.cterm_of thy
       |> Thm.weaken_sorts (Variable.sorts_of ctxt);
     val global_result = result |> Future.map
       (Drule.flexflex_unique (SOME ctxt) #>

--- a/src/Pure/more_thm.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/more_thm.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -116,18 +116,21 @@
 
 fun add_cterm_frees ct =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+    val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
-  in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end;
+  in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.cterm_of thy v) | _ => I) t end;
 
 
 (* cterm constructors and destructors *)
 
 fun all_name (x, t) A =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm t);
+    val thy = Thm.theory_of_cterm t;
     val T = Thm.typ_of_cterm t;
-  in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
+  in
+    Thm.apply (Thm.cterm_of thy (Const ("Pure.all", (T --> propT) --> propT)))
+      (Thm.lambda_name (x, t) A)
+  end;
 
 fun all t A = all_name ("", t) A;
 

--- a/src/Pure/subgoal.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/subgoal.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -67,7 +67,6 @@
 *)
 fun lift_import idx params th ctxt =
   let
-    val cert = Proof_Context.cterm_of ctxt;
     val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
 
     val Ts = map Thm.typ_of_cterm params;
@@ -86,7 +85,8 @@
           else (Ts ---> T, ts);
         val u = Free (y, U);
         in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
-    val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys));
+    val (inst1, inst2) =
+      split_list (map (apply2 (apply2 (Proof_Context.cterm_of ctxt))) (map2 var_inst vars ys));
 
     val th'' = Thm.instantiate ([], inst1) th';
   in ((inst2, th''), ctxt'') end;

--- a/src/Pure/variable.ML	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/variable.ML	Thu Mar 05 13:28:04 2015 +0100
@@ -587,9 +587,9 @@
 
 fun focus_cterm goal ctxt =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
+    val thy = Thm.theory_of_cterm goal;
     val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
-    val ps' = map (cert o Free) ps;
+    val ps' = map (Thm.cterm_of thy o Free) ps;
     val goal' = fold forall_elim_prop ps' goal;
   in ((xs ~~ ps', goal'), ctxt') end;