# HG changeset patch
# User wenzelm
# Date 1425645574 -3600
# Node ID e6939796717e4e4d6b73e748fdbc8e5bdc4890c1
# Parent  b60e65ad13df45f6540d10f6733e2c137e55a0de
clarified context;

diff -r b60e65ad13df -r e6939796717e src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/function_context_tree.ML
--- a/src/HOL/Tools/Function/function_context_tree.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/relation.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 13:39:34 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 b60e65ad13df -r e6939796717e src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 06 13:39:34 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)