# HG changeset patch
# User wenzelm
# Date 1425646868 -3600
# Node ID 92d7d8e4f1bf7c7b0987e1bede5921a4a4d438bd
# Parent  fdfdf89a83a6185953f9ebec28fd3a170ee3dddb# Parent  9f89bdd74a918ad1d4ad1e0313b2fdda5df95931
merged

diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -213,11 +213,13 @@
 
 fun cterm_instantiate_pos cts thm =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+    val thy = Thm.theory_of_thm thm;
     val vars = Term.add_vars (Thm.prop_of thm) [];
     val vars' = rev (drop (length vars - length cts) vars);
-    val ps = map_filter (fn (_, NONE) => NONE
-      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+    val ps =
+      map_filter
+        (fn (_, NONE) => NONE
+          | (var, SOME ct) => SOME (Thm.cterm_of thy (Var var), ct)) (vars' ~~ cts);
   in
     Drule.cterm_instantiate ps thm
   end;
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/fun_cases.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -19,7 +19,6 @@
 
 fun mk_fun_cases ctxt prop =
   let
-    val thy = Proof_Context.theory_of ctxt;
     fun err () =
       error (Pretty.string_of (Pretty.block
         [Pretty.str "Proposition is not a function equation:",
@@ -30,7 +29,7 @@
     val info = Function.get_info ctxt f handle List.Empty => err ();
     val {elims, pelims, is_partial, ...} = info;
     val elims = if is_partial then pelims else the elims;
-    val cprop = Thm.cterm_of thy prop;
+    val cprop = Proof_Context.cterm_of ctxt prop;
     fun mk_elim rl =
       Thm.implies_intr cprop
         (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -325,9 +325,9 @@
         elims = Option.map (map fact) elims, pelims = map fact pelims }
     end
 
-fun lift_morphism thy f =
+fun lift_morphism ctxt f =
   let
-    fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
+    fun term t = Thm.term_of (Drule.cterm_rule f (Proof_Context.cterm_of ctxt t))
   in
     Morphism.morphism "lift_morphism"
       {binding = [],
@@ -338,13 +338,12 @@
 
 fun import_function_data t ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val ct = Thm.cterm_of thy t
-    val inst_morph = lift_morphism thy o Thm.instantiate
+    val ct = Proof_Context.cterm_of ctxt t
+    val inst_morph = lift_morphism ctxt o Thm.instantiate
 
     fun match (trm, data) =
-      SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of thy trm, ct))))
-      handle Pattern.MATCH => NONE
+      SOME (transform_function_data data (inst_morph (Thm.match (Proof_Context.cterm_of ctxt trm, ct))))
+        handle Pattern.MATCH => NONE
   in
     get_first match (Item_Net.retrieve (get_functions ctxt) t)
   end
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/function_context_tree.ML
--- a/src/HOL/Tools/Function/function_context_tree.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -20,11 +20,11 @@
 
   val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree
 
-  val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
+  val inst_tree: Proof.context -> term -> term -> ctx_tree -> ctx_tree
 
   val export_term : ctxt -> term -> term
-  val export_thm : theory -> ctxt -> thm -> thm
-  val import_thm : theory -> ctxt -> thm -> thm
+  val export_thm : Proof.context -> ctxt -> thm -> thm
+  val import_thm : Proof.context -> ctxt -> thm -> thm
 
   val traverse_tree :
    (ctxt -> term ->
@@ -116,16 +116,14 @@
         val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
         val (c, subs) = (Thm.concl_of r, Thm.prems_of r)
 
-        val subst =
-          Pattern.match (Proof_Context.theory_of ctxt) (c, tt') (Vartab.empty, Vartab.empty)
+        val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
         val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
-        val inst = map (fn v =>
-            (Thm.cterm_of thy (Var v), Thm.cterm_of thy (Envir.subst_term subst (Var v))))
-          (Term.add_vars c [])
+        val inst =
+          map (fn v => apply2 (Proof_Context.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
+            (Term.add_vars c [])
       in
-         (cterm_instantiate inst r, dep, branches)
-      end
-      handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
+        (cterm_instantiate inst r, dep, branches)
+      end handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
   | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
 
 
@@ -158,10 +156,10 @@
     mk_tree' ctxt t
   end
 
-fun inst_tree thy fvar f tr =
+fun inst_tree ctxt fvar f tr =
   let
-    val cfvar = Thm.cterm_of thy fvar
-    val cf = Thm.cterm_of thy f
+    val cfvar = Proof_Context.cterm_of ctxt fvar
+    val cf = Proof_Context.cterm_of ctxt f
 
     fun inst_term t =
       subst_bound(f, abstract_over (fvar, t))
@@ -174,7 +172,7 @@
       | inst_tree_aux (RCall (t, str)) =
         RCall (inst_term t, inst_tree_aux str)
     and inst_branch ((fxs, assms), str) =
-      ((fxs, map (Thm.assume o Thm.cterm_of thy o inst_term o Thm.prop_of) assms),
+      ((fxs, map (Thm.assume o Proof_Context.cterm_of ctxt o inst_term o Thm.prop_of) assms),
        inst_tree_aux str)
   in
     inst_tree_aux tr
@@ -188,12 +186,12 @@
  fold_rev (curry Logic.mk_implies o Thm.prop_of) assumes
  #> fold_rev (Logic.all o Free) fixes
 
-fun export_thm thy (fixes, assumes) =
+fun export_thm ctxt (fixes, assumes) =
  fold_rev (Thm.implies_intr o Thm.cprop_of) assumes
- #> fold_rev (Thm.forall_intr o Thm.cterm_of thy o Free) fixes
+ #> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) fixes
 
-fun import_thm thy (fixes, athms) =
- fold (Thm.forall_elim o Thm.cterm_of thy o Free) fixes
+fun import_thm ctxt (fixes, athms) =
+ fold (Thm.forall_elim o Proof_Context.cterm_of ctxt o Free) fixes
  #> fold Thm.elim_implies athms
 
 
@@ -242,19 +240,18 @@
 
 fun rewrite_by_tree ctxt h ih x tr =
   let
-    val thy = Proof_Context.theory_of ctxt
-    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Thm.cterm_of thy t), x)
+    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Proof_Context.cterm_of ctxt t), x)
       | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
         let
           val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
 
-          val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+          val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
             |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
                                                     (* (a, h a) : G   *)
-          val inst_ih = instantiate' [] [SOME (Thm.cterm_of thy arg)] ih
+          val inst_ih = instantiate' [] [SOME (Proof_Context.cterm_of ctxt arg)] ih
           val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
 
-          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of thy h)) inner
+          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Proof_Context.cterm_of ctxt h)) inner
           val h_a_eq_f_a = eq RS eq_reflection
           val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
         in
@@ -269,12 +266,12 @@
                 |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
                 |> filter_out Thm.is_reflexive
 
-              val assumes' = map (simplify (put_simpset HOL_basic_ss  ctxt addsimps used)) assumes
+              val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
 
               val (subeq, x') =
                 rewrite_help (fix @ fixes) (h_as @ assumes') x st
               val subeq_exp =
-                export_thm thy (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
+                export_thm ctxt (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
             in
               (subeq_exp, x')
             end
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -145,17 +145,16 @@
     val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 
-    val thy = Proof_Context.theory_of ctxt'
-
     fun inst t = subst_bounds (rev qs, t)
     val gs = map inst pre_gs
     val lhs = inst pre_lhs
     val rhs = inst pre_rhs
 
-    val cqs = map (Thm.cterm_of thy) qs
-    val ags = map (Thm.assume o Thm.cterm_of thy) gs
+    val cqs = map (Proof_Context.cterm_of ctxt') qs
+    val ags = map (Thm.assume o Proof_Context.cterm_of ctxt') gs
 
-    val case_hyp = Thm.assume (Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+    val case_hyp =
+      Thm.assume (Proof_Context.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   in
     ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
       cqs = cqs, ags = ags, case_hyp = case_hyp }
@@ -183,11 +182,10 @@
     val Globals {h, ...} = globals
 
     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
-    val cert = Proof_Context.cterm_of ctxt
 
     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
     val lGI = GIntro_thm
-      |> Thm.forall_elim (cert f)
+      |> Thm.forall_elim (Proof_Context.cterm_of ctxt f)
       |> fold Thm.forall_elim cqs
       |> fold Thm.elim_implies ags
 
@@ -195,7 +193,7 @@
       let
         val llRI = RI
           |> fold Thm.forall_elim cqs
-          |> fold (Thm.forall_elim o cert o Free) rcfix
+          |> fold (Thm.forall_elim o Proof_Context.cterm_of ctxt o Free) rcfix
           |> fold Thm.elim_implies ags
           |> fold Thm.elim_implies rcassm
 
@@ -262,7 +260,6 @@
 (* Generates the replacement lemma in fully quantified form. *)
 fun mk_replacement_lemma ctxt h ih_elim clause =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
       RCs, tree, ...} = clause
     local open Conv in
@@ -274,7 +271,7 @@
 
     val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
     val h_assums = map (fn RCInfo {h_assum, ...} =>
-      Thm.assume (Thm.cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+      Thm.assume (Proof_Context.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs
 
     val (eql, _) =
       Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree
@@ -343,12 +340,12 @@
 
     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
-      |> fold_rev (Thm.forall_intr o Thm.cterm_of thy o Free) RIvs
+      |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) RIvs
 
     val existence = fold (curry op COMP o prep_RC) RCs lGI
 
-    val P = Thm.cterm_of thy (mk_eq (y, rhsC))
-    val G_lhs_y = Thm.assume (Thm.cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+    val P = Proof_Context.cterm_of ctxt (mk_eq (y, rhsC))
+    val G_lhs_y = Thm.assume (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
     val unique_clauses =
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
@@ -359,19 +356,21 @@
       |> Seq.list_of |> the_single
 
     val uniqueness = G_cases
-      |> Thm.forall_elim (Thm.cterm_of thy lhs)
-      |> Thm.forall_elim (Thm.cterm_of thy y)
+      |> Thm.forall_elim (Proof_Context.cterm_of ctxt lhs)
+      |> Thm.forall_elim (Proof_Context.cterm_of ctxt y)
       |> Thm.forall_elim P
       |> Thm.elim_implies G_lhs_y
       |> fold elim_implies_eta unique_clauses
       |> Thm.implies_intr (Thm.cprop_of G_lhs_y)
-      |> Thm.forall_intr (Thm.cterm_of thy y)
+      |> Thm.forall_intr (Proof_Context.cterm_of ctxt y)
 
-    val P2 = Thm.cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+    val P2 = Proof_Context.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
     val exactly_one =
       @{thm ex1I}
-      |> instantiate' [SOME (Thm.ctyp_of thy ranT)] [SOME P2, SOME (Thm.cterm_of thy rhsC)]
+      |> instantiate'
+          [SOME (Proof_Context.ctyp_of ctxt ranT)]
+          [SOME P2, SOME (Proof_Context.cterm_of ctxt rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
       |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
@@ -383,8 +382,8 @@
       existence
       |> Thm.implies_intr ihyp
       |> Thm.implies_intr (Thm.cprop_of case_hyp)
-      |> Thm.forall_intr (Thm.cterm_of thy x)
-      |> Thm.forall_elim (Thm.cterm_of thy lhs)
+      |> Thm.forall_intr (Proof_Context.cterm_of ctxt x)
+      |> Thm.forall_elim (Proof_Context.cterm_of ctxt lhs)
       |> curry (op RS) refl
   in
     (exactly_one, function_value)
@@ -394,19 +393,18 @@
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
   let
     val Globals {h, domT, ranT, x, ...} = globals
-    val thy = Proof_Context.theory_of ctxt
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
     val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
-      |> Thm.cterm_of thy
+      |> Proof_Context.cterm_of ctxt
 
     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
-      |> instantiate' [] [NONE, SOME (Thm.cterm_of thy h)]
+      |> instantiate' [] [NONE, SOME (Proof_Context.cterm_of ctxt h)]
 
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
@@ -423,11 +421,12 @@
       |> Thm.forall_elim_vars 0
       |> fold (curry op COMP) ex1s
       |> Thm.implies_intr (ihyp)
-      |> Thm.implies_intr (Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
-      |> Thm.forall_intr (Thm.cterm_of thy x)
+      |> Thm.implies_intr (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+      |> Thm.forall_intr (Proof_Context.cterm_of ctxt x)
       |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
       |> (fn it =>
-          fold (Thm.forall_intr o Thm.cterm_of thy o Var) (Term.add_vars (Thm.prop_of it) []) it)
+          fold (Thm.forall_intr o Proof_Context.cterm_of ctxt o Var)
+            (Term.add_vars (Thm.prop_of it) []) it)
 
     val goalstate =  Conjunction.intr graph_is_function complete
       |> Thm.close_derivation
@@ -458,7 +457,6 @@
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val cert = Proof_Context.cterm_of lthy
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
@@ -468,7 +466,7 @@
           #> the_default ("", 0)
       in
         fold_rev (fn Free (n, T) =>
-          forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
+          forall_intr_rename (n, Proof_Context.cterm_of lthy (Var (varmap (n, T), T)))) qs thm
       end
   in
     ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
@@ -533,7 +531,7 @@
 
 fun fix_globals domT ranT fvar ctxt =
   let
-    val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
+    val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes
       ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   in
     (Globals {h = Free (h, domT --> ranT),
@@ -565,19 +563,20 @@
 
 fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function =
   let
-    val thy = Proof_Context.theory_of ctxt
     val Globals {domT, z, ...} = globals
 
     fun mk_psimp
       (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
       let
-        val lhs_acc = Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
-        val z_smaller = Thm.cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+        val lhs_acc =
+          Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+        val z_smaller =
+          Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
       in
         ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
         |> (fn it => it COMP graph_is_function)
         |> Thm.implies_intr z_smaller
-        |> Thm.forall_intr (Thm.cterm_of thy z)
+        |> Thm.forall_intr (Proof_Context.cterm_of ctxt  z)
         |> (fn it => it COMP valthm)
         |> Thm.implies_intr lhs_acc
         |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff])
@@ -705,12 +704,11 @@
 (* FIXME: broken by design *)
 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
       qglr = (oqs, _, _, _), ...} = clause
     val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
       |> fold_rev (curry Logic.mk_implies) gs
-      |> Thm.cterm_of thy
+      |> Proof_Context.cterm_of ctxt
   in
     Goal.init goal
     |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the
@@ -730,7 +728,6 @@
 
 fun mk_nest_term_case ctxt globals R' ihyp clause =
   let
-    val thy = Proof_Context.theory_of ctxt
     val Globals {z, ...} = globals
     val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
       qglr=(oqs, _, _, _), ...} = clause
@@ -740,23 +737,23 @@
     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
       let
         val used = (u @ sub)
-          |> map (fn (ctxt, thm) => Function_Context_Tree.export_thm thy ctxt thm)
+          |> map (fn (ctx, thm) => Function_Context_Tree.export_thm ctxt ctx thm)
 
         val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *)
           |> Function_Context_Tree.export_term (fixes, assumes)
           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags
           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-          |> Thm.cterm_of thy
+          |> Proof_Context.cterm_of ctxt
 
         val thm = Thm.assume hyp
           |> fold Thm.forall_elim cqs
           |> fold Thm.elim_implies ags
-          |> Function_Context_Tree.import_thm thy (fixes, assumes)
+          |> Function_Context_Tree.import_thm ctxt (fixes, assumes)
           |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
 
         val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
-          |> Thm.cterm_of thy |> Thm.assume
+          |> Proof_Context.cterm_of ctxt |> Thm.assume
 
         val acc = thm COMP ih_case
         val z_acc_local = acc
@@ -764,7 +761,7 @@
               (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
 
         val ethm = z_acc_local
-          |> Function_Context_Tree.export_thm thy (fixes,
+          |> Function_Context_Tree.export_thm ctxt (fixes,
                z_eq_arg :: case_hyp :: ags @ assumes)
           |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
 
@@ -780,7 +777,6 @@
 
 fun mk_nest_term_rule ctxt globals R R_cases clauses =
   let
-    val thy = Proof_Context.theory_of ctxt
     val Globals { domT, x, z, ... } = globals
     val acc_R = mk_acc domT R
 
@@ -792,42 +788,42 @@
 
     val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
       (domT --> domT --> boolT) --> boolT) $ R')
-      |> Thm.cterm_of thy (* "wf R'" *)
+      |> Proof_Context.cterm_of ctxt (* "wf R'" *)
 
     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
     val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
-      |> Thm.cterm_of thy
+      |> Proof_Context.cterm_of ctxt
 
     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
 
-    val R_z_x = Thm.cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+    val R_z_x = Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x))
 
     val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
   in
     R_cases
-    |> Thm.forall_elim (Thm.cterm_of thy z)
-    |> Thm.forall_elim (Thm.cterm_of thy x)
-    |> Thm.forall_elim (Thm.cterm_of thy (acc_R $ z))
+    |> Thm.forall_elim (Proof_Context.cterm_of ctxt z)
+    |> Thm.forall_elim (Proof_Context.cterm_of ctxt x)
+    |> Thm.forall_elim (Proof_Context.cterm_of ctxt (acc_R $ z))
     |> curry op COMP (Thm.assume R_z_x)
     |> fold_rev (curry op COMP) cases
     |> Thm.implies_intr R_z_x
-    |> Thm.forall_intr (Thm.cterm_of thy z)
+    |> Thm.forall_intr (Proof_Context.cterm_of ctxt z)
     |> (fn it => it COMP accI)
     |> Thm.implies_intr ihyp
-    |> Thm.forall_intr (Thm.cterm_of thy x)
+    |> Thm.forall_intr (Proof_Context.cterm_of ctxt x)
     |> (fn it => Drule.compose (it, 2, wf_induct_rule))
     |> curry op RS (Thm.assume wfR')
     |> forall_intr_vars
     |> (fn it => it COMP allI)
     |> fold Thm.implies_intr hyps
     |> Thm.implies_intr wfR'
-    |> Thm.forall_intr (Thm.cterm_of thy R')
-    |> Thm.forall_elim (Thm.cterm_of thy (inrel_R))
+    |> Thm.forall_intr (Proof_Context.cterm_of ctxt R')
+    |> Thm.forall_elim (Proof_Context.cterm_of ctxt (inrel_R))
     |> curry op RS wf_in_rel
     |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
-    |> Thm.forall_intr (Thm.cterm_of thy Rrel)
+    |> Thm.forall_intr (Proof_Context.cterm_of ctxt Rrel)
   end
 
 
@@ -865,7 +861,7 @@
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
     val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
-    val trees = map (Function_Context_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
+    val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
@@ -877,18 +873,16 @@
     val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
 
-    val cert = Proof_Context.cterm_of lthy
-
     val xclauses = PROFILE "xclauses"
       (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
         RCss GIntro_thms) RIntro_thmss
 
     val complete =
-      mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
+      mk_completeness globals clauses abstract_qglrs |> Proof_Context.cterm_of lthy |> Thm.assume
 
     val compat =
       mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
-      |> map (cert #> Thm.assume)
+      |> map (Proof_Context.cterm_of lthy #> Thm.assume)
 
     val compat_store = store_compat_thms n compat
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -80,7 +80,6 @@
 fun mk_partial_elim_rules ctxt result =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
     val n_fs = length fs;
@@ -116,12 +115,12 @@
         val args = HOLogic.mk_tuple arg_vars;
         val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
 
-        val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
+        val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
         val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
 
-        val cprop = cert prop;
+        val cprop = Proof_Context.cterm_of ctxt prop;
 
-        val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+        val asms = [cprop, Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
         val asms_thms = map Thm.assume asms;
 
         fun prep_subgoal_tac i =
@@ -134,10 +133,10 @@
         val elim_stripped =
           nth cases idx
           |> Thm.forall_elim P
-          |> Thm.forall_elim (cert args)
+          |> Thm.forall_elim (Proof_Context.cterm_of ctxt args)
           |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
           |> fold_rev Thm.implies_intr asms
-          |> Thm.forall_intr (cert rhs_var);
+          |> Thm.forall_intr (Proof_Context.cterm_of ctxt rhs_var);
 
         val bool_elims =
           (case ranT of
@@ -146,7 +145,7 @@
 
         fun unstrip rl =
           rl
-          |> fold_rev (Thm.forall_intr o cert) arg_vars
+          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) arg_vars
           |> Thm.forall_intr P
       in
         map unstrip (elim_stripped :: bool_elims)
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -105,7 +105,7 @@
    val ty = fastype_of t
  in
    Goal.prove_internal ctxt []
-     (Thm.cterm_of thy
+     (Proof_Context.cterm_of ctxt
        (Logic.mk_equals (t,
           if null is
           then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -204,9 +204,6 @@
 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
   (IndScheme {T, cases=scases, branches}) =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val cert = Thm.cterm_of thy
-
     val n = length branches
     val scases_idx = map_index I scases
 
@@ -224,7 +221,7 @@
           $ (HOLogic.pair_const T T $ Bound 0 $ x)
           $ R),
          HOLogic.mk_Trueprop (P_comp $ Bound 0)))
-      |> cert
+      |> Proof_Context.cterm_of ctxt
 
     val aihyp = Thm.assume ihyp
 
@@ -237,9 +234,10 @@
     fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
       let
         val fxs = map Free xs
-        val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+        val branch_hyp =
+          Thm.assume (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
 
-        val C_hyps = map (cert #> Thm.assume) Cs
+        val C_hyps = map (Proof_Context.cterm_of ctxt #> Thm.assume) Cs
 
         val (relevant_cases, ineqss') =
           (scases_idx ~~ ineqss)
@@ -249,10 +247,11 @@
         fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
           let
             val case_hyps =
-              map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+              map (Thm.assume o Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq)
+                (fxs ~~ lhs)
 
-            val cqs = map (cert o Free) qs
-            val ags = map (Thm.assume o cert) gs
+            val cqs = map (Proof_Context.cterm_of ctxt o Free) qs
+            val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
 
             val replace_x_simpset =
               put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
@@ -260,16 +259,16 @@
 
             fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
               let
-                val cGas = map (Thm.assume o cert) Gas
-                val cGvs = map (cert o Free) Gvs
+                val cGas = map (Thm.assume o Proof_Context.cterm_of ctxt) Gas
+                val cGvs = map (Proof_Context.cterm_of ctxt o Free) Gvs
                 val import = fold Thm.forall_elim (cqs @ cGvs)
                   #> fold Thm.elim_implies (ags @ cGas)
                 val ipres = pres
-                  |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
+                  |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P_of idx, rcargs)))
                   |> import
               in
                 sih
-                |> Thm.forall_elim (cert (inject idx rcargs))
+                |> Thm.forall_elim (Proof_Context.cterm_of ctxt (inject idx rcargs))
                 |> Thm.elim_implies (import ineq) (* Psum rcargs *)
                 |> Conv.fconv_rule (sum_prod_conv ctxt)
                 |> Conv.fconv_rule (ind_rulify ctxt)
@@ -284,7 +283,7 @@
               |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
               |> fold_rev (curry Logic.mk_implies) gs
               |> fold_rev (Logic.all o Free) qs
-              |> cert
+              |> Proof_Context.cterm_of ctxt
 
             val Plhs_to_Pxs_conv =
               foldl1 (uncurry Conv.combination_conv)
@@ -304,14 +303,15 @@
         val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
 
         val bstep = complete_thm
-          |> Thm.forall_elim (cert (list_comb (P, fxs)))
-          |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
+          |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P, fxs)))
+          |> fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) (fxs @ map Free ws)
           |> fold Thm.elim_implies C_hyps
           |> fold Thm.elim_implies cases (* P xs *)
           |> fold_rev (Thm.implies_intr o Thm.cprop_of) C_hyps
-          |> fold_rev (Thm.forall_intr o cert o Free) ws
+          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) ws
 
-        val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
+        val Pxs =
+          Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (P_comp $ x))
           |> Goal.init
           |> (Simplifier.rewrite_goals_tac ctxt
                 (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
@@ -320,7 +320,7 @@
           |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
           |> Goal.finish ctxt
           |> Thm.implies_intr (Thm.cprop_of branch_hyp)
-          |> fold_rev (Thm.forall_intr o cert) fxs
+          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) fxs
       in
         (Pxs, steps)
       end
@@ -332,7 +332,7 @@
     val istep = sum_split_rule
       |> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
       |> Thm.implies_intr ihyp
-      |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+      |> Thm.forall_intr (Proof_Context.cterm_of ctxt x) (* "!!x. (!!y<x. P y) ==> P x" *)
 
     val induct_rule =
       @{thm "wf_induct_rule"}
@@ -351,15 +351,17 @@
   let
     val (ctxt', _, cases, concl) = dest_hhf ctxt t
     val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
-    val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
+    val ([Rn, xn], ctxt'') = Variable.variant_fixes ["R", "x"] ctxt'
     val R = Free (Rn, mk_relT ST)
     val x = Free (xn, ST)
-    val cert = Proof_Context.cterm_of ctxt
 
-    val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
+    val ineqss =
+      mk_ineqs R scheme
+      |> map (map (apply2 (Thm.assume o Proof_Context.cterm_of ctxt'')))
     val complete =
-      map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
-    val wf_thm = mk_wf R scheme |> cert |> Thm.assume
+      map_range (mk_completeness ctxt'' scheme #> Proof_Context.cterm_of ctxt'' #> Thm.assume)
+        (length branches)
+    val wf_thm = mk_wf R scheme |> Proof_Context.cterm_of ctxt'' |> Thm.assume
 
     val (descent, pres) = split_list (flat ineqss)
     val newgoals = complete @ pres @ wf_thm :: descent
@@ -371,7 +373,7 @@
       let
         val inst = (foldr1 HOLogic.mk_prod (map Free xs))
           |> Sum_Tree.mk_inj ST (length branches) (i + 1)
-          |> cert
+          |> Proof_Context.cterm_of ctxt''
       in
         indthm
         |> Drule.instantiate' [] [SOME inst]
@@ -386,7 +388,7 @@
     val nbranches = length branches
     val npres = length pres
   in
-    Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
+    Thm.bicompose (SOME ctxt'') {flatten = false, match = false, incremented = false}
       (false, res, length newgoals) i
     THEN term_tac (i + nbranches + npres)
     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -66,9 +66,9 @@
     fold_rev Logic.all vars (Logic.list_implies (prems, concl))
   end
 
-fun mk_cell thy solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
+fun mk_cell ctxt solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
   let
-    val goals = Thm.cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
+    val goals = Proof_Context.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
   in
     case try_proof (goals @{const_name Orderings.less}) solve_tac of
       Solved thm => Less thm
@@ -175,7 +175,6 @@
 
 fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
   let
-    val thy = Proof_Context.theory_of ctxt
     val ((_ $ (_ $ rel)) :: tl) = Thm.prems_of st
 
     val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
@@ -184,7 +183,7 @@
       Measure_Functions.get_measure_functions ctxt domT
 
     val table = (* 2: create table *)
-      map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+      map (fn t => map (mk_cell ctxt solve_tac (dest_term t)) measure_funs) tl
   in
     fn st =>
       case search_table table of
@@ -201,10 +200,11 @@
             else ()
   
         in (* 4: proof reconstruction *)
-          st |> (PRIMITIVE (cterm_instantiate [(Thm.cterm_of thy rel, Thm.cterm_of thy relation)])
-          THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
-          THEN (rtac @{thm "wf_empty"} 1)
-          THEN EVERY (map prove_row clean_table))
+          st |>
+          (PRIMITIVE (cterm_instantiate [apply2 (Proof_Context.cterm_of ctxt) (rel, relation)])
+            THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+            THEN (rtac @{thm "wf_empty"} 1)
+            THEN EVERY (map prove_row clean_table))
         end
   end) 1 st;
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -149,8 +149,6 @@
 
 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
   let
-    val thy = Proof_Context.theory_of ctxt
-
     val oqnames = map fst pre_qs
     val (qs, _) = Variable.variant_fixes oqnames ctxt
       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
@@ -160,8 +158,8 @@
     val args = map inst pre_args
     val rhs = inst pre_rhs
 
-    val cqs = map (Thm.cterm_of thy) qs
-    val ags = map (Thm.assume o Thm.cterm_of thy) gs
+    val cqs = map (Proof_Context.cterm_of ctxt) qs
+    val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
 
     val import = fold Thm.forall_elim cqs
       #> fold Thm.elim_implies ags
@@ -198,10 +196,10 @@
 
 fun mk_applied_form ctxt caTs thm =
   let
-    val thy = Proof_Context.theory_of ctxt
     val xs =
       map_index (fn (i, T) =>
-        Thm.cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
+        Proof_Context.cterm_of ctxt
+          (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   in
     fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
     |> Conv.fconv_rule (Thm.beta_conversion true)
@@ -211,7 +209,6 @@
 
 fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
   let
-    val cert = Proof_Context.cterm_of ctxt
     val newPs =
       map2 (fn Pname => fn MutualPart {cargTs, ...} =>
           Free (Pname, cargTs ---> HOLogic.boolT))
@@ -229,7 +226,7 @@
     val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
 
     val induct_inst =
-      Thm.forall_elim (cert case_exp) induct
+      Thm.forall_elim (Proof_Context.cterm_of ctxt case_exp) induct
       |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
       |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
 
@@ -239,9 +236,9 @@
         val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
       in
         (rule
-         |> Thm.forall_elim (cert inj)
+         |> Thm.forall_elim (Proof_Context.cterm_of ctxt inj)
          |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
-         |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
+         |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) (afs @ newPs),
          k + length cargTs)
       end
   in
@@ -261,8 +258,7 @@
     val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
     val (args, name_ctxt) = mk_var "x" argsT name_ctxt
     
-    val cert = Proof_Context.cterm_of ctxt
-    val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
+    val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
     val sumtree_inj = Sum_Tree.mk_inj ST n i args
 
     val sum_elims =
@@ -274,9 +270,9 @@
   in
     cases_rule
     |> Thm.forall_elim P
-    |> Thm.forall_elim (cert sumtree_inj)
+    |> Thm.forall_elim (Proof_Context.cterm_of ctxt sumtree_inj)
     |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal)
-    |> Thm.forall_intr (cert args)
+    |> Thm.forall_intr (Proof_Context.cterm_of ctxt args)
     |> Thm.forall_intr P
   end
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -40,12 +40,13 @@
    (avs, pvs, j)
  end
 
-fun filter_pats thy cons pvars [] = []
-  | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
-  | filter_pats thy cons pvars (((pat as Free _) :: pats, thm) :: pts) =
-    let val inst = list_comb (cons, pvars)
-    in (inst :: pats, inst_free (Thm.cterm_of thy pat) (Thm.cterm_of thy inst) thm)
-       :: (filter_pats thy cons pvars pts)
+fun filter_pats ctxt cons pvars [] = []
+  | filter_pats ctxt cons pvars (([], thm) :: pts) = raise Match
+  | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) =
+    let val inst = list_comb (cons, pvars) in
+      (inst :: pats,
+        inst_free (Proof_Context.cterm_of ctxt pat) (Proof_Context.cterm_of ctxt inst) thm)
+        :: (filter_pats ctxt cons pvars pts)
     end
   | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
     if fst (strip_comb pat) = cons
@@ -55,65 +56,66 @@
 
 fun transform_pat _ avars c_assum ([] , thm) = raise Match
   | transform_pat ctxt avars c_assum (pat :: pats, thm) =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val (_, subps) = strip_comb pat
-    val eqs = map (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
-    val c_eq_pat = simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
-  in
-    (subps @ pats,
-     fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
-  end
+      let
+        val (_, subps) = strip_comb pat
+        val eqs =
+          map (Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+        val c_eq_pat =
+          simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
+      in
+        (subps @ pats,
+         fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
+      end
 
 
 exception COMPLETENESS
 
 fun constr_case ctxt P idx (v :: vs) pats cons =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val (avars, pvars, newidx) = invent_vars cons idx
-    val c_hyp = Thm.cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
-    val c_assum = Thm.assume c_hyp
-    val newpats = map (transform_pat ctxt avars c_assum) (filter_pats thy cons pvars pats)
-  in
-    o_alg ctxt P newidx (avars @ vs) newpats
-    |> Thm.implies_intr c_hyp
-    |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) avars
-  end
+      let
+        val (avars, pvars, newidx) = invent_vars cons idx
+        val c_hyp =
+          Proof_Context.cterm_of ctxt
+            (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
+        val c_assum = Thm.assume c_hyp
+        val newpats = map (transform_pat ctxt avars c_assum) (filter_pats ctxt cons pvars pats)
+      in
+        o_alg ctxt P newidx (avars @ vs) newpats
+        |> Thm.implies_intr c_hyp
+        |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) avars
+      end
   | constr_case _ _ _ _ _ _ = raise Match
 and o_alg _ P idx [] (([], Pthm) :: _)  = Pthm
   | o_alg _ P idx (v :: vs) [] = raise COMPLETENESS
   | o_alg ctxt P idx (v :: vs) pts =
-  if forall (is_Free o hd o fst) pts (* Var case *)
-  then o_alg ctxt P idx vs
-         (map (fn (pv :: pats, thm) =>
-           (pats, refl RS
-            (inst_free (Proof_Context.cterm_of ctxt pv)
-              (Proof_Context.cterm_of ctxt v) thm))) pts)
-  else (* Cons case *)
-    let
-      val thy = Proof_Context.theory_of ctxt
-      val T as Type (tname, _) = fastype_of v
-      val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
-      val constrs = inst_constrs_of ctxt T
-      val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
-    in
-      inst_case_thm thy v P case_thm
-      |> fold (curry op COMP) c_cases
-    end
+      if forall (is_Free o hd o fst) pts (* Var case *)
+      then o_alg ctxt P idx vs
+             (map (fn (pv :: pats, thm) =>
+               (pats, refl RS
+                (inst_free (Proof_Context.cterm_of ctxt pv)
+                  (Proof_Context.cterm_of ctxt v) thm))) pts)
+      else (* Cons case *)
+        let
+          val thy = Proof_Context.theory_of ctxt
+          val T as Type (tname, _) = fastype_of v
+          val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
+          val constrs = inst_constrs_of ctxt T
+          val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
+        in
+          inst_case_thm thy v P case_thm
+          |> fold (curry op COMP) c_cases
+        end
   | o_alg _ _ _ _ _ = raise Match
 
 fun prove_completeness ctxt xs P qss patss =
   let
-    val thy = Proof_Context.theory_of ctxt
     fun mk_assum qs pats =
       HOLogic.mk_Trueprop P
       |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
       |> fold_rev Logic.all qs
-      |> Thm.cterm_of thy
+      |> Proof_Context.cterm_of ctxt
 
     val hyps = map2 mk_assum qss patss
-    fun inst_hyps hyp qs = fold (Thm.forall_elim o Thm.cterm_of thy) qs (Thm.assume hyp)
+    fun inst_hyps hyp qs = fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) qs (Thm.assume hyp)
     val assums = map2 inst_hyps hyps qss
     in
       o_alg ctxt P 2 xs (patss ~~ assums)
@@ -122,7 +124,6 @@
 
 fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   let
-    val thy = Proof_Context.theory_of ctxt
     val (vs, subgf) = dest_all_all subgoal
     val (cases, _ $ thesis) = Logic.strip_horn subgf
       handle Bind => raise COMPLETENESS
@@ -141,7 +142,7 @@
 
     val patss = map (map snd) x_pats
     val complete_thm = prove_completeness ctxt xs thesis qss patss
-      |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) vs
+      |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) vs
     in
       PRIMITIVE (fn st => Drule.compose (complete_thm, i, st))
   end
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/relation.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -16,10 +16,11 @@
 (* tactic version *)
 
 fun inst_state_tac inst st =
-  (case Term.add_vars (Thm.prop_of st) [] of
+  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
     [v as (_, T)] =>
-      let val cert = Thm.cterm_of (Thm.theory_of_thm st);
-      in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
+      let val thy = Thm.theory_of_thm st in
+        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of thy (Var v), Thm.cterm_of thy (inst T))])) st
+      end
   | _ => Seq.empty);
 
 fun relation_tac ctxt rel i =
@@ -30,17 +31,16 @@
 (* version with type inference *)
 
 fun inst_state_infer_tac ctxt rel st =
-  (case Term.add_vars (Thm.prop_of st) [] of
+  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
     [v as (_, T)] =>
       let
-        val cert = Proof_Context.cterm_of ctxt;
         val rel' = singleton (Variable.polymorphic ctxt) rel
           |> map_types Type_Infer.paramify_vars
           |> Type.constraint T
           |> Syntax.check_term ctxt
-          |> cert;
+          |> Proof_Context.cterm_of ctxt;
       in
-        PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st
+        PRIMITIVE (Thm.instantiate ([], [(Proof_Context.cterm_of ctxt (Var v), rel')])) st
       end
   | _ => Seq.empty);
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -272,7 +272,7 @@
     val level_mapping =
       map_index pt_lev lev
         |> Termination.mk_sumcases D (setT nat_pairT)
-        |> Thm.cterm_of thy
+        |> Proof_Context.cterm_of ctxt
     in
       PROFILE "Proof Reconstruction"
         (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
@@ -307,7 +307,7 @@
 fun gen_decomp_scnp_tac orders autom_tac ctxt =
   Termination.TERMINATION ctxt autom_tac (fn D =>
     let
-      val decompose = Termination.decompose_tac D
+      val decompose = Termination.decompose_tac ctxt D
       val scnp_full = single_scnp_tac true orders ctxt D
     in
       REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -29,7 +29,7 @@
 
   val wf_union_tac : Proof.context -> tactic
 
-  val decompose_tac : ttac
+  val decompose_tac : Proof.context -> ttac
 end
 
 
@@ -137,14 +137,14 @@
     mk_skel (fold collect_pats cs [])
   end
 
-fun prove_chain thy chain_tac (c1, c2) =
+fun prove_chain ctxt chain_tac (c1, c2) =
   let
     val goal =
       HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
         Const (@{const_abbrev Set.empty}, fastype_of c1))
       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   in
-    case Function_Lib.try_proof (Thm.cterm_of thy goal) chain_tac of
+    case Function_Lib.try_proof (Proof_Context.cterm_of ctxt goal) chain_tac of
       Function_Lib.Solved thm => SOME thm
     | _ => NONE
   end
@@ -166,10 +166,10 @@
 
 fun dest_call (sk, _, _, _, _) = dest_call' sk
 
-fun mk_desc thy tac vs Gam l r m1 m2 =
+fun mk_desc ctxt tac vs Gam l r m1 m2 =
   let
     fun try rel =
-      try_proof (Thm.cterm_of thy
+      try_proof (Proof_Context.cterm_of ctxt
         (Logic.list_all (vs,
            Logic.mk_implies (HOLogic.mk_Trueprop Gam,
              HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
@@ -187,23 +187,24 @@
      | _ => raise Match
 end
 
-fun prove_descent thy tac sk (c, (m1, m2)) =
+fun prove_descent ctxt tac sk (c, (m1, m2)) =
   let
     val (vs, _, l, _, r, Gam) = dest_call' sk c
   in 
-    mk_desc thy tac vs Gam l r m1 m2
+    mk_desc ctxt tac vs Gam l r m1 m2
   end
 
 fun create ctxt chain_tac descent_tac T rel =
   let
-    val thy = Proof_Context.theory_of ctxt
     val sk = mk_sum_skel rel
     val Ts = node_types sk T
     val M = Inttab.make (map_index (apsnd (Measure_Functions.get_measure_functions ctxt)) Ts)
-    val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
-      (prove_chain thy chain_tac)
-    val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
-      (prove_descent thy descent_tac sk)
+    val chain_cache =
+      Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
+        (prove_chain ctxt chain_tac)
+    val descent_cache =
+      Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
+        (prove_descent ctxt descent_tac sk)
   in
     (sk, nth Ts, M, chain_cache, descent_cache)
   end
@@ -275,7 +276,6 @@
 fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
   let
     val thy = Proof_Context.theory_of ctxt
-    val cert = Thm.cterm_of thy
     val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st
 
     fun mk_compr ineq =
@@ -302,7 +302,7 @@
           THEN' (blast_tac ctxt)))    (* Solve rest of context... not very elegant *)
       ) i
   in
-    (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
+    (PRIMITIVE (Drule.cterm_instantiate [apply2 (Proof_Context.cterm_of ctxt) (rel, relation)])
      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
      THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
   end) 1 st
@@ -326,7 +326,7 @@
     ORELSE' rtac @{thm union_comp_emptyL}
     ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
 
-fun regroup_calls_tac cs = CALLS (fn (cs', i) =>
+fun regroup_calls_tac ctxt cs = CALLS (fn (cs', i) =>
  let
    val is = map (fn c => find_index (curry op aconv c) cs') cs
  in
@@ -342,14 +342,14 @@
    | _ => no_tac)
   | _ => no_tac)
 
-fun decompose_tac D = CALLS (fn (cs, i) =>
+fun decompose_tac ctxt D = CALLS (fn (cs, i) =>
   let
     val G = mk_dgraph D cs
     val sccs = Term_Graph.strong_conn G
 
     fun split [SCC] i = TRY (solve_trivial_tac D i)
       | split (SCC::rest) i =
-        regroup_calls_tac SCC i
+        regroup_calls_tac ctxt SCC i
         THEN rtac @{thm wf_union_compatible} i
         THEN rtac @{thm less_by_empty} (i + 2)
         THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -352,10 +352,10 @@
 in  
   fun freeze_spec th ctxt =
     let
-      val cert = Proof_Context.cterm_of ctxt;
       val ([x], ctxt') =
         Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
-      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
+      val spec' = spec
+        |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
     in (th RS spec', ctxt') end
 end;
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -398,21 +398,19 @@
   (case Thm.tpairs_of th of
     [] => th
   | pairs =>
-    let
-      val thy = Thm.theory_of_thm th
-      val cert = Thm.cterm_of thy
-      val certT = Thm.ctyp_of thy
-      val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-
-      fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
-      fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
-
-      val instsT = Vartab.fold (cons o mkT) tyenv []
-      val insts = Vartab.fold (cons o mk) tenv []
-    in
-      Thm.instantiate (instsT, insts) th
-    end
-    handle THM _ => th)
+      let
+        val thy = Thm.theory_of_thm th
+        val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+  
+        fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (v, S), T)
+        fun mk (v, (T, t)) = apply2 (Thm.cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+  
+        val instsT = Vartab.fold (cons o mkT) tyenv []
+        val insts = Vartab.fold (cons o mk) tenv []
+      in
+        Thm.instantiate (instsT, insts) th
+      end
+      handle THM _ => th)
 
 fun is_metis_literal_genuine (_, (s, _)) =
   not (String.isPrefix class_prefix (Metis_Name.toString s))
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -609,8 +609,6 @@
     val (indrule_lemma_prems, indrule_lemma_concls) =
       split_list (map2 mk_indrule_lemma descr' recTs);
 
-    val cert = Thm.cterm_of thy6;
-
     val indrule_lemma =
       Goal.prove_sorry_global thy6 [] []
         (Logic.mk_implies
@@ -627,7 +625,8 @@
     val frees =
       if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
       else map (Free o apfst fst o dest_Var) Ps;
-    val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
+    val indrule_lemma' =
+      cterm_instantiate (map (Thm.cterm_of thy6) Ps ~~ map (Thm.cterm_of thy6) frees) indrule_lemma;
 
     val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
     val dt_induct =
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -126,7 +126,7 @@
 
 fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
+    val thy = Thm.theory_of_cterm cgoal;
     val goal = Thm.term_of cgoal;
     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule));
     val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
@@ -148,7 +148,8 @@
       map_filter (fn (t, u) =>
         (case abstr (getP u) of
           NONE => NONE
-        | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
+        | SOME u' =>
+            SOME (apply2 (Thm.cterm_of thy) (t |> getP |> snd |> head_of, u')))) (ts ~~ ts');
     val indrule' = cterm_instantiate insts indrule;
   in resolve0_tac [indrule'] i end);
 
@@ -157,7 +158,6 @@
 
 fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
   let
-    val thy = Thm.theory_of_cterm cgoal;
     val goal = Thm.term_of cgoal;
     val params = Logic.strip_params goal;
     val (_, Type (tname, _)) = hd (rev params);
@@ -166,8 +166,8 @@
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     val exhaustion' =
       cterm_instantiate
-        [(Thm.cterm_of thy (head_of lhs),
-          Thm.cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
+        [apply2 (Proof_Context.cterm_of ctxt)
+          (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
         exhaustion;
   in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -46,8 +46,7 @@
           Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
             Var (("P", 0), HOLogic.boolT));
         val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
-        val cert = Thm.cterm_of thy;
-        val insts' = map cert induct_Ps ~~ map cert insts;
+        val insts' = map (Thm.cterm_of thy) induct_Ps ~~ map (Thm.cterm_of thy) insts;
         val induct' =
           refl RS
             (nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
@@ -204,11 +203,12 @@
             Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
               absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
                 (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
-        val cert = Thm.cterm_of thy1;
         val insts =
           map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
             ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
-        val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
+        val induct' = induct
+          |> cterm_instantiate
+            (map (Thm.cterm_of thy1) induct_Ps ~~ map (Thm.cterm_of thy1) insts);
       in
         Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
           (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
@@ -379,9 +379,9 @@
 
     fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
       let
-        val cert = Thm.cterm_of thy;
         val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
-        val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
+        val exhaustion' = exhaustion
+          |> cterm_instantiate [apply2 (Thm.cterm_of thy) (lhs, Free ("x", T))];
         fun tac ctxt =
           EVERY [resolve_tac ctxt [exhaustion'] 1,
             ALLGOALS (asm_simp_tac
@@ -450,10 +450,10 @@
       let
         val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
         val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
-        val cert = Thm.cterm_of thy;
         val nchotomy' = nchotomy RS spec;
         val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
-        val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
+        val nchotomy'' =
+          cterm_instantiate [apply2 (Thm.cterm_of thy) (Var v, Ma)] nchotomy';
       in
         Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
           (fn {context = ctxt, prems, ...} =>
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -89,24 +89,25 @@
       (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
     val Type (_, [_, iT]) = T;
     val icT = Thm.ctyp_of thy iT;
-    val cert = Thm.cterm_of thy;
     val inst = Thm.instantiate_cterm ([(aT, icT)], []);
     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     val t_rhs = lambda t_k proto_t_rhs;
     val eqs0 = [subst_v @{term "0::natural"} eq,
       subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
-    val ((_, (_, eqs2)), lthy') = BNF_LFP_Compat.add_primrec_simple
-      [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
+    val ((_, (_, eqs2)), lthy') = lthy
+      |> BNF_LFP_Compat.add_primrec_simple
+        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;
     val rule = @{thm random_aux_rec}
-      |> Drule.instantiate_normalize ([(aT, icT)],
-           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
+      |> Drule.instantiate_normalize
+        ([(aT, icT)],
+          [(cT_random_aux, Thm.cterm_of thy t_random_aux), (cT_rhs, Thm.cterm_of thy t_rhs)]);
     fun tac ctxt =
       ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
-      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
+      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
     val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
   in (simp, lthy') end;
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -108,15 +108,13 @@
 
 fun match_instantiateT ctxt t thm =
   if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
-    let val certT = Proof_Context.ctyp_of ctxt
-    in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
+    Thm.instantiate (gen_certify_inst fst TVar (Proof_Context.ctyp_of ctxt) ctxt thm t, []) thm
   else thm
 
 fun match_instantiate ctxt t thm =
-  let
-    val cert = Proof_Context.cterm_of ctxt
-    val thm' = match_instantiateT ctxt t thm
-  in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
+  let val thm' = match_instantiateT ctxt t thm in
+    Thm.instantiate ([], gen_certify_inst snd Var (Proof_Context.cterm_of ctxt) ctxt thm' t) thm'
+  end
 
 fun apply_rule ctxt t =
   (case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/code_evaluation.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -204,13 +204,13 @@
 
 fun certify_eval ctxt value conv ct =
   let
-    val cert = Proof_Context.cterm_of ctxt;
     val t = Thm.term_of ct;
     val T = fastype_of t;
-    val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
+    val mk_eq =
+      Thm.mk_binop (Proof_Context.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
   in case value ctxt t
    of NONE => Thm.reflexive ct
-    | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
+    | SOME t' => conv ctxt (mk_eq ct (Proof_Context.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
         handle THM _ =>
           error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
   end;
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -27,7 +27,6 @@
 fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val cert = Thm.cterm_of thy;
 
     val recTs = Old_Datatype_Aux.get_rec_types descr;
     val pnames =
@@ -106,11 +105,11 @@
         (map (fn ((((i, _), T), U), tname) =>
           make_pred i U T (mk_proj i is r) (Free (tname, T)))
             (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
-    val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
+    val inst = map (apply2 (Thm.cterm_of thy)) (map head_of (HOLogic.dest_conj
       (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
 
     val thm =
-      Goal.prove_internal ctxt (map cert prems) (cert concl)
+      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems) (Thm.cterm_of thy concl)
         (fn prems =>
            EVERY [
             rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -160,7 +159,6 @@
 fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val cert = Thm.cterm_of thy;
     val rT = TFree ("'P", @{sort type});
     val rT' = TVar (("'P", 0), @{sort type});
 
@@ -187,11 +185,12 @@
     val y' = Free ("y", T);
 
     val thm =
-      Goal.prove_internal ctxt (map cert prems)
-        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
+      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems)
+        (Thm.cterm_of thy
+          (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
         (fn prems =>
            EVERY [
-            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
+            rtac (cterm_instantiate [apply2 (Thm.cterm_of thy) (y, y')] exhaust) 1,
             ALLGOALS (EVERY'
               [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
                resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/record.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -1460,8 +1460,6 @@
   avoid problems with higher order unification.*)
 fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
-
     val g = Thm.term_of cgoal;
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
@@ -1475,7 +1473,7 @@
       | [x] => (head_of x, false));
     val rule'' =
       cterm_instantiate
-        (map (apply2 cert)
+        (map (apply2 (Proof_Context.cterm_of ctxt))
           (case rev params of
             [] =>
               (case AList.lookup (op =) (Term.add_frees g []) s of
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/HOL/Tools/reification.ML
--- a/src/HOL/Tools/reification.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/reification.ML	Fri Mar 06 14:01:08 2015 +0100
@@ -48,7 +48,6 @@
   let
     val Const (fN, _) = th |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
       |> fst |> strip_comb |> fst;
-    val cert = Proof_Context.cterm_of ctxt;
     val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
     fun add_fterms (t as t1 $ t2) =
@@ -84,7 +83,7 @@
         (fn {context, prems, ...} =>
           Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym;
     val (cong' :: vars') =
-      Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs);
+      Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Proof_Context.cterm_of ctxt'') vs);
     val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
 
   in (vs', cong') end;
@@ -134,8 +133,6 @@
 fun decomp_reify da cgns (ct, ctxt) bds =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
     fun tryabsdecomp (ct, ctxt) bds =
       (case Thm.term_of ct of
         Abs (_, xT, ta) =>
@@ -143,8 +140,8 @@
             val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
             val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta);  (* FIXME !? *)
             val x = Free (xn, xT);
-            val cx = cert x;
-            val cta = cert ta;
+            val cx = Proof_Context.cterm_of ctxt' x;
+            val cta = Proof_Context.cterm_of ctxt' ta;
             val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
                 NONE => error "tryabsdecomp: Type not found in the Environement"
               | SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
@@ -172,10 +169,12 @@
           val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
           val (fts, its) =
             (map (snd o snd) fnvs,
-             map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t)) invs);
-          val ctyenv = map (fn ((vn, vi), (s, ty)) => (certT (TVar((vn, vi), s)), certT ty)) (Vartab.dest tyenv);
+             map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t)) invs);
+          val ctyenv =
+            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of thy) (TVar ((vn, vi), s), ty))
+              (Vartab.dest tyenv);
         in
-          ((map cert fts ~~ replicate (length fts) ctxt,
+          ((map (Thm.cterm_of thy) fts ~~ replicate (length fts) ctxt,
              apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
         end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
   end;
@@ -196,8 +195,6 @@
         val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt;
         val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt';
         val thy = Proof_Context.theory_of ctxt'';
-        val cert = Thm.cterm_of thy;
-        val certT = Thm.ctyp_of thy;
         val vsns_map = vss ~~ vsns;
         val xns_map = fst (split_list nths) ~~ xns;
         val subst = map (fn (nt, xn) => (nt, Var ((xn, 0), fastype_of nt))) xns_map;
@@ -205,15 +202,15 @@
         val (tyenv, tmenv) = Pattern.match thy (rhs_P, Thm.term_of ct) (Vartab.empty, Vartab.empty);
         val sbst = Envir.subst_term (tyenv, tmenv);
         val sbsT = Envir.subst_type tyenv;
-        val subst_ty = map (fn (n, (s, t)) =>
-          (certT (TVar (n, s)), certT t)) (Vartab.dest tyenv)
+        val subst_ty =
+          map (fn (n, (s, t)) => apply2 (Thm.ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
         val tml = Vartab.dest tmenv;
         val (subst_ns, bds) = fold_map
           (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
             let
               val name = snd (the (AList.lookup (op =) tml xn0));
               val (idx, bds) = index_of name bds;
-            in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds;
+            in (apply2 (Thm.cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
         val subst_vs =
           let
             fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
@@ -222,12 +219,13 @@
                 val lT' = sbsT lT;
                 val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
                 val vsn = the (AList.lookup (op =) vsns_map vs);
-                val cvs = cert (fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT')));
-              in (cert vs, cvs) end;
+                val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
+              in apply2 (Thm.cterm_of thy) (vs, vs') end;
           in map h subst end;
-        val cts = map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t))
-          (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
-            (map (fn n => (n, 0)) xns) tml);
+        val cts =
+          map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t))
+            (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
+              (map (fn n => (n, 0)) xns) tml);
         val substt =
           let
             val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
@@ -261,15 +259,17 @@
       |> fst)) eqs [];
     val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
     val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
-    val cert = Proof_Context.cterm_of ctxt';
     val subst =
-      the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs);
+      the o AList.lookup (op =)
+        (map2 (fn T => fn v => (T, Proof_Context.cterm_of ctxt' (Free (v, T)))) tys vs);
     fun prep_eq eq =
       let
         val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
           |> HOLogic.dest_eq |> fst |> strip_comb;
-        val subst = map_filter (fn (v as Var (_, T)) => SOME (cert v, subst T)
-          | _ => NONE) vs;
+        val subst =
+          map_filter
+            (fn (v as Var (_, T)) => SOME (Proof_Context.cterm_of ctxt' v, subst T)
+              | _ => NONE) vs;
       in Thm.instantiate ([], subst) eq end;
     val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
     val bds = AList.make (K ([], [])) tys;
@@ -285,10 +285,9 @@
       | is_list_var _ = false;
     val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd
       |> strip_comb |> snd |> filter is_list_var;
-    val cert = Proof_Context.cterm_of ctxt;
     val vs = map (fn v as Var (_, T) =>
       (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
-    val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
+    val th' = Drule.instantiate_normalize ([], map (apply2 (Proof_Context.cterm_of ctxt)) vs) th;
     val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
   in Thm.transitive th'' th' end;
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/element.ML	Fri Mar 06 14:01:08 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
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/expression.ML	Fri Mar 06 14:01:08 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
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/generic_target.ML	Fri Mar 06 14:01:08 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*)
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/obtain.ML	Fri Mar 06 14:01:08 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
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/proof.ML	Fri Mar 06 14:01:08 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 =>
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 06 14:01:08 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)
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 06 14:01:08 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;
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/drule.ML	Fri Mar 06 14:01:08 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;
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/goal.ML	Fri Mar 06 14:01:08 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) #>
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/more_thm.ML	Fri Mar 06 14:01:08 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;
 
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/subgoal.ML	Fri Mar 06 14:01:08 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;
diff -r fdfdf89a83a6 -r 92d7d8e4f1bf src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/variable.ML	Fri Mar 06 14:01:08 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;