# HG changeset patch
# User wenzelm
# Date 1425682603 -3600
# Node ID 929984c529d390626192c02cd3af9a656fec02dd
# Parent  a2d056424d3ce07e3def96604170fae00ba6c705
clarified context;

diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -469,7 +469,7 @@
       val T = mk_tupleT_balanced tfrees;
     in
       @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
-      |> Drule.instantiate' [SOME (Thm.global_ctyp_of @{theory} T)] []
+      |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
       |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
       |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
       |> Thm.varifyT_global
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -222,7 +222,6 @@
 
 fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
   let
-    val thy = Thm.theory_of_thm thm
     val prop = Thm.prop_of thm
     val (t, mk_prop') = dest prop
     (* Only consider "op =" at non-base types *)
@@ -238,7 +237,7 @@
     val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
-    val cprop = Thm.global_cterm_of thy prop2
+    val cprop = Thm.cterm_of ctxt prop2
     val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
@@ -317,7 +316,6 @@
 
 fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
   let
-    val thy = Thm.theory_of_thm thm
     val prop = Thm.prop_of thm
     val (t, mk_prop') = dest prop
     val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
@@ -331,7 +329,7 @@
     val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
     val prop2 = Logic.list_rename_params (rev names) prop1
-    val cprop = Thm.global_cterm_of thy prop2
+    val cprop = Thm.cterm_of ctxt prop2
     val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   in
@@ -415,60 +413,59 @@
 
 fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
   let
-    val thy = Proof_Context.theory_of ctxt
     (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
     fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
-        let
-          val r1 = rel T1 U1
-          val r2 = rel T2 U2
-          val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
-        in
-          Const (@{const_name rel_fun}, rT) $ r1 $ r2
-        end
+          let
+            val r1 = rel T1 U1
+            val r2 = rel T2 U2
+            val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
+          in
+            Const (@{const_name rel_fun}, rT) $ r1 $ r2
+          end
       | rel T U =
-        let
-          val (a, _) = dest_TFree (prj (T, U))
-        in
-          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
-        end
+          let
+            val (a, _) = dest_TFree (prj (T, U))
+          in
+            Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
+          end
     fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
       | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
-        let
-          val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
-          val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
-          val cprop = Thm.global_cterm_of thy (HOLogic.mk_Trueprop prop)
-          val thm0 = Thm.assume cprop
-          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
-          val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
-          val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
-          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
-          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
-          val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
-          val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
-          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
-          val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
-        in
-          (thm2 COMP rule, hyps)
-        end
+          let
+            val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
+            val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
+            val cprop = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop prop)
+            val thm0 = Thm.assume cprop
+            val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
+            val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
+            val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
+            val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
+            val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
+            val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
+            val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
+            val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
+            val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
+          in
+            (thm2 COMP rule, hyps)
+          end
       | zip ctxt thms (f $ t) (g $ u) =
-        let
-          val (thm1, hyps1) = zip ctxt thms f g
-          val (thm2, hyps2) = zip ctxt thms t u
-        in
-          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
-        end
+          let
+            val (thm1, hyps1) = zip ctxt thms f g
+            val (thm2, hyps2) = zip ctxt thms t u
+          in
+            (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
+          end
       | zip _ _ t u =
-        let
-          val T = fastype_of t
-          val U = fastype_of u
-          val prop = mk_Rel (rel T U) $ t $ u
-          val cprop = Thm.global_cterm_of thy (HOLogic.mk_Trueprop prop)
-        in
-          (Thm.assume cprop, [cprop])
-        end
+          let
+            val T = fastype_of t
+            val U = fastype_of u
+            val prop = mk_Rel (rel T U) $ t $ u
+            val cprop = Thm.cterm_of ctxt (HOLogic.mk_Trueprop prop)
+          in
+            (Thm.assume cprop, [cprop])
+          end
     val r = mk_Rel (rel (fastype_of t) (fastype_of u))
     val goal = HOLogic.mk_Trueprop (r $ t $ u)
-    val rename = Thm.trivial (Thm.global_cterm_of thy goal)
+    val rename = Thm.trivial (Thm.cterm_of ctxt goal)
     val (thm, hyps) = zip ctxt [] t u
   in
     Drule.implies_intr_list hyps (thm RS rename)
@@ -577,10 +574,8 @@
     val cbool = @{ctyp bool}
     val relT = @{typ "bool => bool => bool"}
     val idx = Thm.maxidx_of thm + 1
-    val thy = Proof_Context.theory_of ctxt
-    fun tinst (a, _) = (Thm.global_ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
-    fun inst (a, t) =
-      (Thm.global_cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), Thm.global_cterm_of thy t)
+    fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
+    fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
   in
     thm
       |> Thm.generalize (tfrees, rnames @ frees) idx
@@ -603,10 +598,8 @@
     val cbool = @{ctyp bool}
     val relT = @{typ "bool => bool => bool"}
     val idx = Thm.maxidx_of thm + 1
-    val thy = Proof_Context.theory_of ctxt
-    fun tinst (a, _) = (Thm.global_ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
-    fun inst (a, t) =
-      (Thm.global_cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), Thm.global_cterm_of thy t)
+    fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
+    fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
   in
     thm
       |> Thm.generalize (tfrees, rnames @ frees) idx
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -83,7 +83,7 @@
     val ctxt = Proof_Context.init_global thy
 
     val rew_imps = alt_props |>
-      map (Object_Logic.atomize ctxt o Thm.global_cterm_of thy o Syntax.read_prop_global thy o snd)
+      map (Object_Logic.atomize ctxt o Thm.cterm_of ctxt o Syntax.read_prop_global thy o snd)
     val props' = rew_imps |>
       map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of)
 
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/cnf.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -259,14 +259,13 @@
 
 fun make_under_quantifiers ctxt make t =
   let
-    val thy = Proof_Context.theory_of ctxt
     fun conv ctxt ct =
       (case Thm.term_of ct of
         Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
       | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
       | Const _ => Conv.all_conv ct
       | t => make t RS eq_reflection)
-  in conv ctxt (Thm.global_cterm_of thy t) RS meta_eq_to_obj_eq end
+  in conv ctxt (Thm.cterm_of ctxt t) RS meta_eq_to_obj_eq end
 
 fun make_nnf_thm_under_quantifiers ctxt =
   make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -105,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 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj
+    val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
       (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
 
     val thm =
-      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl)
+      Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
         (fn prems =>
            EVERY [
             rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -185,12 +185,12 @@
     val y' = Free ("y", T);
 
     val thm =
-      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems)
-        (Thm.global_cterm_of thy
+      Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems)
+        (Thm.cterm_of ctxt
           (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
         (fn prems =>
            EVERY [
-            rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, y')] exhaust) 1,
+            rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (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 a2d056424d3c -r 929984c529d3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -565,15 +565,13 @@
 
 fun mk_cases ctxt prop =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     fun err msg =
       error (Pretty.string_of (Pretty.block
         [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
 
     val elims = Induct.find_casesP ctxt prop;
 
-    val cprop = Thm.global_cterm_of thy prop;
+    val cprop = Thm.cterm_of ctxt prop;
     fun mk_elim rl =
       Thm.implies_intr cprop
         (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
@@ -636,7 +634,7 @@
       | _ => error
         ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
     val inst =
-      map (fn v => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy (Envir.subst_term subst (Var v))))
+      map (fn v => apply2 (Thm.cterm_of ctxt') (Var v, Envir.subst_term subst (Var v)))
         (Term.add_vars (lhs_of eq) []);
   in
     Drule.cterm_instantiate inst eq
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -41,10 +41,9 @@
 fun strong_ind_simproc tab =
   Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn ctxt => fn t =>
     let
-      val thy = Proof_Context.theory_of ctxt;
       fun close p t f =
         let val vs = Term.add_vars t []
-        in Drule.instantiate' [] (rev (map (SOME o Thm.global_cterm_of thy o Var) vs))
+        in Drule.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
       fun mkop @{const_name HOL.conj} T x =
@@ -93,8 +92,8 @@
             in
               if forall is_none rews then NONE
               else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
-                (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.global_cterm_of thy)
-                   rews ts) (Thm.reflexive (Thm.global_cterm_of thy h)))
+                (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt)
+                   rews ts) (Thm.reflexive (Thm.cterm_of ctxt h)))
             end
         | NONE => NONE)
       | _ => NONE
@@ -200,7 +199,7 @@
 (* 3. simplify                                                *)
 (**************************************************************)
 
-fun mk_to_pred_inst thy fs =
+fun mk_to_pred_inst ctxt fs =
   map (fn (x, ps) =>
     let
       val (Ts, T) = strip_type (fastype_of x);
@@ -208,8 +207,8 @@
       val x' = map_type
         (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
     in
-      (Thm.global_cterm_of thy x,
-       Thm.global_cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+      (Thm.cterm_of ctxt x,
+       Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
          (HOLogic.Collect_const U $
             HOLogic.mk_psplits ps U HOLogic.boolT
               (list_comb (x', map Bound (length Ts - 1 downto 0))))))
@@ -217,8 +216,7 @@
 
 fun mk_to_pred_eq ctxt p fs optfs' T thm =
   let
-    val thy = Thm.theory_of_thm thm;
-    val insts = mk_to_pred_inst thy fs;
+    val insts = mk_to_pred_inst ctxt fs;
     val thm' = Thm.instantiate ([], insts) thm;
     val thm'' =
       (case optfs' of
@@ -233,7 +231,7 @@
               Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb
           in
             thm' RS (Drule.cterm_instantiate [(arg_cong_f,
-              Thm.global_cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
+              Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
                 HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
                   HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
           end)
@@ -322,7 +320,8 @@
         lookup_rule (Proof_Context.theory_of ctxt) (Thm.prop_of #> Logic.dest_equals) rules')
   end;
 
-fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
+fun to_pred_proc thy rules t =
+  case lookup_rule thy I rules t of
     NONE => NONE
   | SOME (lhs, rhs) =>
       SOME (Envir.subst_term
@@ -337,7 +336,7 @@
     val fs = filter (is_Var o fst)
       (infer_arities thy set_arities (NONE, Thm.prop_of thm) []);
     (* instantiate each set parameter with {(x, y). p x y} *)
-    val insts = mk_to_pred_inst thy fs
+    val insts = mk_to_pred_inst ctxt fs
   in
     thm |>
     Thm.instantiate ([], insts) |>
@@ -370,8 +369,8 @@
         val T = HOLogic.mk_ptupleT ps Us;
         val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
       in
-        (Thm.global_cterm_of thy x,
-         Thm.global_cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+        (Thm.cterm_of ctxt x,
+         Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
           (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
              list_comb (x', map Bound (l - 1 downto k + 1))))))
       end) fs;
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/monomorph.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -157,9 +157,9 @@
 
 (* collecting instances *)
 
-fun instantiate thy subst =
+fun instantiate ctxt subst =
   let
-    fun cert (ix, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (ix, S), T)
+    fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T)
     fun cert' subst = Vartab.fold (cons o cert) subst []
   in Thm.instantiate (cert' subst, []) end
 
@@ -186,7 +186,7 @@
         raise ENOUGH cx
       else
         let
-          val thm' = instantiate thy subst thm
+          val thm' = instantiate ctxt subst thm
           val rthm = ((round, subst), thm')
           val rthms = Inttab.lookup_list insts id;
           val n_insts' =
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/numeral.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -44,10 +44,10 @@
 val oneT = Thm.ctyp_of_cterm one;
 
 val numeral = @{cpat "numeral"};
-val numeralT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
+val numeralT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm numeral));
 
 val uminus = @{cpat "uminus"};
-val uminusT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
+val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus));
 
 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
 
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -483,7 +483,7 @@
     simplify_one ctxt (([th, cancel_th]) MRS trans);
 
 local
-  val Tp_Eq = Thm.reflexive (Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop)
+  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop)
   fun Eq_True_elim Eq = 
     Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
 in
@@ -492,9 +492,8 @@
       val zero = Const(@{const_name Groups.zero}, T);
       val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
       val pos = less $ zero $ t and neg = less $ t $ zero
-      val thy = Proof_Context.theory_of ctxt
       fun prove p =
-        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.global_cterm_of thy p)))
+        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p)))
         handle THM _ => NONE
     in case prove pos of
          SOME th => SOME(th RS pos_th)
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/record.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -1375,9 +1375,9 @@
 
     fun mk_split_free_tac free induct_thm i =
       let
-        val cfree = Thm.global_cterm_of thy free;
+        val cfree = Thm.cterm_of ctxt free;
         val _$ (_ $ r) = Thm.concl_of induct_thm;
-        val crec = Thm.global_cterm_of thy r;
+        val crec = Thm.cterm_of ctxt r;
         val thm = cterm_instantiate [(crec, cfree)] induct_thm;
       in
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
@@ -1606,7 +1606,7 @@
       (roughly) the definition of the accessor.*)
     val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
       let
-        val cterm_ext = Thm.global_cterm_of defs_thy ext;
+        val cterm_ext = Thm.cterm_of defs_ctxt ext;
         val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
         val tactic1 =
           simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
@@ -1943,8 +1943,8 @@
               fun to_Var (Free (c, T)) = Var ((c, 1), T);
             in mk_rec (map to_Var all_vars_more) 0 end;
 
-          val cterm_rec = Thm.global_cterm_of ext_thy r_rec0;
-          val cterm_vrs = Thm.global_cterm_of ext_thy r_rec0_Vars;
+          val cterm_rec = Thm.cterm_of ext_ctxt r_rec0;
+          val cterm_vrs = Thm.cterm_of ext_ctxt r_rec0_Vars;
           val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
           val init_thm = named_cterm_instantiate insts updacc_eq_triv;
           val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/reification.ML
--- a/src/HOL/Tools/reification.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/reification.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -169,12 +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)) => apply2 (Thm.global_cterm_of thy) (Var ((vn, vi), tT), t)) invs);
+             map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs);
           val ctyenv =
-            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.global_ctyp_of thy) (TVar ((vn, vi), s), ty))
+            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty))
               (Vartab.dest tyenv);
         in
-          ((map (Thm.global_cterm_of thy) fts ~~ replicate (length fts) ctxt,
+          ((map (Thm.cterm_of ctxt) 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;
@@ -203,14 +203,14 @@
         val sbst = Envir.subst_term (tyenv, tmenv);
         val sbsT = Envir.subst_type tyenv;
         val subst_ty =
-          map (fn (n, (s, t)) => apply2 (Thm.global_ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
+          map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (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 (apply2 (Thm.global_cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
+            in (apply2 (Thm.cterm_of ctxt'') (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
         val subst_vs =
           let
             fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
@@ -220,10 +220,10 @@
                 val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
                 val vsn = the (AList.lookup (op =) vsns_map vs);
                 val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
-              in apply2 (Thm.global_cterm_of thy) (vs, vs') end;
+              in apply2 (Thm.cterm_of ctxt'') (vs, vs') end;
           in map h subst end;
         val cts =
-          map (fn ((vn, vi), (tT, t)) => apply2 (Thm.global_cterm_of thy) (Var ((vn, vi), tT), t))
+          map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt'') (Var ((vn, vi), tT), t))
             (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
               (map (fn n => (n, 0)) xns) tml);
         val substt =
diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/sat.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -73,7 +73,7 @@
 val resolution_thm =
   @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
 
-val cP = Thm.global_cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
+val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT));
 
 (* ------------------------------------------------------------------------- *)
 (* lit_ord: an order on integers that considers their absolute values only,  *)
diff -r a2d056424d3c -r 929984c529d3 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -903,9 +903,8 @@
 
 fun prover ctxt thms Tconcl (js : injust list) split_neq pos : thm option =
   let
-    val thy = Proof_Context.theory_of ctxt
     val nTconcl = LA_Logic.neg_prop Tconcl
-    val cnTconcl = Thm.global_cterm_of thy nTconcl
+    val cnTconcl = Thm.cterm_of ctxt nTconcl
     val nTconclthm = Thm.assume cnTconcl
     val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm])
     val (Falsethm, _) = fwdproof ctxt tree js
diff -r a2d056424d3c -r 929984c529d3 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Provers/hypsubst.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -168,7 +168,6 @@
       Data.dest_Trueprop #> Data.dest_eq #> apply2 contract) (Thm.term_of cBi) of
     SOME (t, t') =>
       let
-        val thy = Proof_Context.theory_of ctxt;
         val Bi = Thm.term_of cBi;
         val ps = Logic.strip_params Bi;
         val U = Term.fastype_of1 (rev (map snd ps), t);
@@ -184,10 +183,10 @@
             (case (if b then t else t') of
               Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
             | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
-        val (instT, _) = Thm.match (apply2 (Thm.global_cterm_of thy o Logic.mk_type) (V, U));
+        val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
       in
         compose_tac ctxt (true, Drule.instantiate_normalize (instT,
-          map (apply2 (Thm.global_cterm_of thy))
+          map (apply2 (Thm.cterm_of ctxt))
             [(Var (ixn, Ts ---> U --> body_type T), u),
              (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
              (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
diff -r a2d056424d3c -r 929984c529d3 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/coherent.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -173,19 +173,16 @@
 
 fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.global_cterm_of thy;
-    val certT = Thm.global_ctyp_of thy;
     val _ =
       cond_trace ctxt (fn () =>
         Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
     val th' =
       Drule.implies_elim_list
         (Thm.instantiate
-           (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
+           (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye),
             map (fn (ixn, (T, t)) =>
-              (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
-            map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
+              apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @
+            map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th)
         (map (nth asms) is);
     val (_, cases) = dest_elim (Thm.prop_of th');
   in
@@ -201,10 +198,8 @@
 
 and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.global_cterm_of thy;
-    val cparams = map cert params;
-    val asms'' = map (cert o curry subst_bounds (rev params)) asms';
+    val cparams = map (Thm.cterm_of ctxt) params;
+    val asms'' = map (Thm.cterm_of ctxt o curry subst_bounds (rev params)) asms';
     val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
   in
     Drule.forall_intr_list cparams
diff -r a2d056424d3c -r 929984c529d3 src/Tools/cong_tac.ML
--- a/src/Tools/cong_tac.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/cong_tac.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -14,7 +14,6 @@
 
 fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
   let
-    val cert = Thm.global_cterm_of (Thm.theory_of_cterm cgoal);
     val goal = Thm.term_of cgoal;
   in
     (case Logic.strip_assums_concl goal of
@@ -25,7 +24,7 @@
           val ps = Logic.strip_params (Thm.concl_of cong');
           val insts =
             [(f', f), (g', g), (x', x), (y', y)]
-            |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
+            |> map (fn (t, u) => apply2 (Thm.cterm_of ctxt) (Term.head_of t, fold_rev Term.abs ps u));
         in
           fn st =>
             compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
diff -r a2d056424d3c -r 929984c529d3 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/eqsubst.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -259,14 +259,11 @@
     val th = Thm.incr_indexes 1 gth;
     val tgt_term = Thm.prop_of th;
 
-    val thy = Thm.theory_of_thm th;
-    val cert = Thm.global_cterm_of thy;
-
     val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
-    val cfvs = rev (map cert fvs);
+    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
 
     val conclterm = Logic.strip_imp_concl fixedbody;
-    val conclthm = Thm.trivial (cert conclterm);
+    val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
     val maxidx = Thm.maxidx_of th;
     val ft =
       (Zipper.move_down_right (* ==> *)
@@ -274,7 +271,7 @@
        o Zipper.mktop
        o Thm.prop_of) conclthm
   in
-    ((cfvs, conclthm), (thy, maxidx, ft))
+    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
   end;
 
 (* substitute using an object or meta level equality *)
diff -r a2d056424d3c -r 929984c529d3 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/nbe.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -580,10 +580,9 @@
 
 fun mk_equals ctxt lhs raw_rhs =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val ty = Thm.typ_of_cterm lhs;
-    val eq = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
-    val rhs = Thm.global_cterm_of thy raw_rhs;
+    val eq = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
+    val rhs = Thm.cterm_of ctxt raw_rhs;
   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result