# HG changeset patch
# User wenzelm
# Date 1433360920 -7200
# Node ID d3f561aa2af654f92913faea349cb47ee14ee760
# Parent  2e1c1968b38e15be06f008aa6107e24ee6b41dc8# Parent  e201bd8973db8d748e513355ae84ecb9cbfab50e
merged

diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -181,7 +181,7 @@
                   val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
 
                   fun label_thm thm =
-                    Thm.cterm_of ctxt' (Free (nm, propT))
+                    Thm.cterm_of ctxt'' (Free (nm, propT))
                     |> Drule.mk_term
                     |> not (null abs_nms) ? Conjunction.intr thm
 
@@ -509,19 +509,18 @@
 (* Fix schematics in the goal *)
 fun focus_concl ctxt i goal =
   let
-    val ({context, concl, params, prems, asms, schematics}, goal') =
+    val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
       Subgoal.focus_params ctxt i goal;
 
-    val ((_, schematic_terms), context') =
-      Variable.import_inst true [Thm.term_of concl] context
-      |>> Thm.certify_inst (Thm.theory_of_thm goal');
+    val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
+    val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
 
     val goal'' = Thm.instantiate ([], schematic_terms) goal';
     val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
     val (schematic_types, schematic_terms') = schematics;
     val schematics' = (schematic_types, schematic_terms @ schematic_terms');
   in
-    ({context = context', concl = concl', params = params, prems = prems,
+    ({context = ctxt'', concl = concl', params = params, prems = prems,
       schematics = schematics', asms = asms} : Subgoal.focus, goal'')
   end;
 
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/GCD.thy	Wed Jun 03 21:48:40 2015 +0200
@@ -1355,7 +1355,7 @@
 
 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
-  by (auto intro: dvd_antisym [transferred] lcm_least_int)  (* FIXME slow *)
+  using lcm_least_int zdvd_antisym_nonneg by auto
 
 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Import/import_rule.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -328,13 +328,14 @@
 
 fun store_thm binding thm thy =
   let
+    val ctxt = Proof_Context.init_global thy
     val thm = Drule.export_without_context_open thm
     val tvs = Term.add_tvars (Thm.prop_of thm) []
     val tns = map (fn (_, _) => "'") tvs
-    val nms = fst (fold_map Name.variant tns (Variable.names_of (Proof_Context.init_global thy)))
+    val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
     val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
-    val cvs = map (Thm.global_ctyp_of thy) vs
-    val ctvs = map (Thm.global_ctyp_of thy) (map TVar tvs)
+    val cvs = map (Thm.ctyp_of ctxt) vs
+    val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
     val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
   in
     snd (Global_Theory.add_thm ((binding, thm'), []) thy)
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -28,7 +28,7 @@
   (*utility functions*)
   val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     Proof.state -> bool
-  val theorems_in_proof_term : thm -> thm list
+  val theorems_in_proof_term : theory -> thm -> thm list
   val theorems_of_sucessful_proof : Toplevel.state option -> thm list
   val get_setting : (string * string) list -> string * string -> string
   val get_int_setting : (string * string) list -> string * int -> int
@@ -178,9 +178,9 @@
 
 in
 
-fun theorems_in_proof_term thm =
+fun theorems_in_proof_term thy thm =
   let
-    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) true
+    val all_thms = Global_Theory.all_thms_of thy true
     fun collect (s, _, _) = if s <> "" then insert (op =) s else I
     fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
     fun resolve_thms names = map_filter (member_of names) all_thms
@@ -195,7 +195,8 @@
     NONE => []
   | SOME st =>
       if not (Toplevel.is_proof st) then []
-      else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
+      else
+        theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st))))
 
 fun get_setting settings (key, default) =
   the_default default (AList.lookup (op =) settings key)
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -120,8 +120,8 @@
 val perm_simproc =
   Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
 
-fun projections rule =
-  Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule
+fun projections ctxt rule =
+  Project_Rule.projections ctxt rule
   |> map (Drule.export_without_context #> Rule_Cases.save rule);
 
 val supp_prod = @{thm supp_prod};
@@ -1114,7 +1114,9 @@
     val (_, thy9) = thy8 |>
       Sign.add_path big_name |>
       Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
-      Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
+      Global_Theory.add_thmss
+        [((Binding.name "inducts", projections (Proof_Context.init_global thy8) dt_induct),
+            [case_names_induct])] ||>
       Sign.parent_path ||>>
       Old_Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
       Old_Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
@@ -1412,7 +1414,9 @@
       Sign.add_path big_name |>
       Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
       Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
-      Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
+      Global_Theory.add_thmss
+        [((Binding.name "strong_inducts", projections (Proof_Context.init_global thy9) induct),
+            [case_names_induct])];
 
     (**** recursion combinator ****)
 
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -145,10 +145,11 @@
     val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
     fun inst_fresh vars params i st =
    let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
-       val thy = Thm.theory_of_thm st;
    in case subtract (op =) vars vars' of
      [x] =>
-      Seq.single (Thm.instantiate ([], [(Thm.global_cterm_of thy x, Thm.global_cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
+      Seq.single
+        (Thm.instantiate ([],
+          [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st)
     | _ => error "fresh_fun_simp: Too many variables, please report."
    end
   in
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -39,8 +39,8 @@
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;
 
-fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
-  (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
+fun mk_perm_bool_simproc names =
+  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
          then SOME perm_bool else NONE
@@ -591,7 +591,7 @@
     val monos = Inductive.get_monos ctxt;
     val intrs' = Inductive.unpartition_rules intrs
       (map (fn (((s, ths), (_, k)), th) =>
-           (s, ths ~~ Inductive.infer_intro_vars th k ths))
+           (s, ths ~~ Inductive.infer_intro_vars thy th k ths))
          (Inductive.partition_rules raw_induct intrs ~~
           Inductive.arities_of raw_induct ~~ elims));
     val k = length (Inductive.params_of raw_induct);
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -43,8 +43,8 @@
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;
 
-fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
-  (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
+fun mk_perm_bool_simproc names =
+  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
          then SOME perm_bool else NONE
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -70,11 +70,6 @@
 val perm_aux_fold       = @{thm "perm_aux_fold"}; 
 val supports_fresh_rule = @{thm "supports_fresh"};
 
-(* pulls out dynamically a thm via the proof state *)
-fun dynamic_thms st name = Global_Theory.get_thms (Thm.theory_of_thm st) name;
-fun dynamic_thm  st name = Global_Theory.get_thm  (Thm.theory_of_thm st) name;
-
-
 (* needed in the process of fully simplifying permutations *)
 val strong_congs = [@{thm "if_cong"}]
 (* needed to avoid warnings about overwritten congs *)
@@ -146,7 +141,7 @@
     ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
     let
        val ctxt' = ctxt
-         addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
+         addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
          addsimprocs [perm_simproc_fun, perm_simproc_app]
          |> fold Simplifier.del_cong weak_congs
          |> fold Simplifier.add_cong strong_congs
@@ -296,7 +291,6 @@
       case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of
           _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
           let
-            val cert = Thm.global_cterm_of (Thm.theory_of_thm st);
             val ps = Logic.strip_params (Thm.term_of goal);
             val Ts = rev (map snd ps);
             val vs = collect_vars 0 x [];
@@ -310,8 +304,8 @@
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (Thm.prems_of supports_rule'));
             val supports_rule'' = Drule.cterm_instantiate
-              [(cert (head_of S), cert s')] supports_rule'
-            val fin_supp = dynamic_thms st ("fin_supp")
+              [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_rule'
+            val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
             val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
           in
             (tactical ctxt ("guessing of the right supports-set",
@@ -332,15 +326,14 @@
 fun fresh_guess_tac_i tactical ctxt i st =
     let 
         val goal = nth (cprems_of st) (i - 1)
-        val fin_supp = dynamic_thms st ("fin_supp")
-        val fresh_atm = dynamic_thms st ("fresh_atm")
+        val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
+        val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
         val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
         val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
     in
       case Logic.strip_assums_concl (Thm.term_of goal) of
           _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => 
           let
-            val cert = Thm.global_cterm_of (Thm.theory_of_thm st);
             val ps = Logic.strip_params (Thm.term_of goal);
             val Ts = rev (map snd ps);
             val vs = collect_vars 0 t [];
@@ -354,7 +347,7 @@
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule'));
             val supports_fresh_rule'' = Drule.cterm_instantiate
-              [(cert (head_of S), cert s')] supports_fresh_rule'
+              [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_fresh_rule'
           in
             (tactical ctxt ("guessing of the right set that supports the goal", 
                       (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Wed Jun 03 21:48:40 2015 +0200
@@ -12,9 +12,8 @@
 subsection {* Export and re-import of global proof terms *}
 
 ML {*
-  fun export_proof thm =
+  fun export_proof thy thm =
     let
-      val thy = Thm.theory_of_thm thm;
       val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
       val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
       val prf =
@@ -40,24 +39,24 @@
 lemma ex: "A \<longrightarrow> A" ..
 
 ML_val {*
-  val xml = export_proof @{thm ex};
+  val xml = export_proof @{theory} @{thm ex};
   val thm = import_proof thy1 xml;
 *}
 
 ML_val {*
-  val xml = export_proof @{thm de_Morgan};
+  val xml = export_proof @{theory} @{thm de_Morgan};
   val thm = import_proof thy1 xml;
 *}
 
 ML_val {*
-  val xml = export_proof @{thm Drinker's_Principle};
+  val xml = export_proof @{theory} @{thm Drinker's_Principle};
   val thm = import_proof thy1 xml;
 *}
 
 text {* Some fairly large proof: *}
 
 ML_val {*
-  val xml = export_proof @{thm abs_less_iff};
+  val xml = export_proof @{theory} @{thm abs_less_iff};
   val thm = import_proof thy1 xml;
   @{assert} (size (YXML.string_of_body xml) > 1000000);
 *}
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -1449,7 +1449,7 @@
                 (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
               |> K |> Goal.prove_sorry lthy [] [] goal
               |> Thm.close_derivation
-              |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
+              |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
                 @{thms eqTrueE eq_False[THEN iffD1] notnotD}
               |> pair eqn_pos
               |> single
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -11,7 +11,7 @@
   val trace : bool Config.T
   val max_clauses : int Config.T
   val term_pair_of: indexname * (typ * 'a) -> term * 'a
-  val first_order_resolve : thm -> thm -> thm
+  val first_order_resolve : Proof.context -> thm -> thm -> thm
   val size_of_subgoals: thm -> int
   val has_too_many_clauses: Proof.context -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
@@ -41,8 +41,8 @@
   val prolog_step_tac': Proof.context -> thm list -> int -> tactic
   val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
   val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
-  val make_meta_clause: thm -> thm
-  val make_meta_clauses: thm list -> thm list
+  val make_meta_clause: Proof.context -> thm -> thm
+  val make_meta_clauses: Proof.context -> thm list -> thm list
   val meson_tac: Proof.context -> thm list -> int -> tactic
 end
 
@@ -98,16 +98,16 @@
 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
 
 (*FIXME: currently does not "rename variables apart"*)
-fun first_order_resolve thA thB =
+fun first_order_resolve ctxt thA thB =
   (case
     try (fn () =>
-      let val thy = Thm.theory_of_thm thA
+      let val thy = Proof_Context.theory_of ctxt
           val tmA = Thm.concl_of thA
           val Const(@{const_name Pure.imp},_) $ tmB $ _ = Thm.prop_of thB
           val tenv =
             Pattern.first_order_match thy (tmB, tmA)
                                           (Vartab.empty, Vartab.empty) |> snd
-          val ct_pairs = map (apply2 (Thm.global_cterm_of thy) o term_pair_of) (Vartab.dest tenv)
+          val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
       in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
     SOME th => th
   | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
@@ -359,11 +359,10 @@
     in (th RS spec', ctxt') end
 end;
 
-fun apply_skolem_theorem (th, rls) =
+fun apply_skolem_theorem ctxt (th, rls) =
   let
     fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
-      | tryall (rl :: rls) =
-        first_order_resolve th rl handle THM _ => tryall rls
+      | tryall (rl :: rls) = first_order_resolve ctxt th rl handle THM _ => tryall rls
   in tryall rls end
 
 (* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
@@ -383,7 +382,7 @@
                 in  ctxt_ref := ctxt'; cnf_aux (th', ths) end
           | Const (@{const_name Ex}, _) =>
               (*existential quantifier: Insert Skolem functions*)
-              cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
+              cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths)
           | Const (@{const_name HOL.disj}, _) =>
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
@@ -787,15 +786,15 @@
     th RS notEfalse handle THM _ => th RS notEfalse';
 
 (*Converting one theorem from a disjunction to a meta-level clause*)
-fun make_meta_clause th =
-  let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
+fun make_meta_clause ctxt th =
+  let val (fth, thaw) = Misc_Legacy.freeze_thaw_robust ctxt th
   in  
       (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
        negated_asm_of_head o make_horn resolution_clause_rules) fth
   end;
 
-fun make_meta_clauses ths =
+fun make_meta_clauses ctxt ths =
     name_thms "MClause#"
-      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
+      (distinct Thm.eq_thm_prop (map (make_meta_clause ctxt) ths));
 
 end;
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -133,7 +133,7 @@
 
 val proxy_defs = map (fst o snd o snd) proxy_table
 fun prepare_helper ctxt =
-  Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
+  Meson.make_meta_clause ctxt #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
 
 fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
   if is_tptp_variable s then
@@ -181,7 +181,7 @@
           SOME s =>
           let val s = s |> space_explode "_" |> tl |> space_implode "_" in
             (case Int.fromString s of
-              SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
+              SOME j => Meson.make_meta_clause ctxt (snd (nth clauses j)) |> Isa_Raw |> some
             | NONE =>
               if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
               else raise Fail ("malformed fact identifier " ^ quote ident))
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -171,11 +171,10 @@
 (* INFERENCE RULE: RESOLVE *)
 
 (*Increment the indexes of only the type variables*)
-fun incr_type_indexes inc th =
+fun incr_type_indexes ctxt inc th =
   let
     val tvs = Term.add_tvars (Thm.full_prop_of th) []
-    val thy = Thm.theory_of_thm th
-    fun inc_tvar ((a, i), s) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
+    fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s))
   in
     Thm.instantiate (map inc_tvar tvs, []) th
   end
@@ -185,7 +184,7 @@
    Instantiations of those Vars could then fail. *)
 fun resolve_inc_tyvars ctxt tha i thb =
   let
-    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
+    val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
     fun res (tha, thb) =
       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
             (false, tha, Thm.nprems_of tha) i thb
@@ -393,16 +392,16 @@
   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
     equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
 
-fun flexflex_first_order th =
+fun flexflex_first_order ctxt th =
   (case Thm.tpairs_of th of
     [] => th
   | pairs =>
       let
-        val thy = Thm.theory_of_thm th
+        val thy = Proof_Context.theory_of ctxt
         val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   
-        fun mkT (v, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (v, S), T)
-        fun mk (v, (T, t)) = apply2 (Thm.global_cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+        fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T)
+        fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t)
   
         val instsT = Vartab.fold (cons o mkT) tyenv []
         val insts = Vartab.fold (cons o mk) tenv []
@@ -462,7 +461,7 @@
       val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
       val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
       val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
-        |> flexflex_first_order
+        |> flexflex_first_order ctxt
         |> resynchronize ctxt fol_th
       val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
       val _ = trace_msg ctxt (fn () => "=============================================")
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -32,8 +32,9 @@
 val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
 
 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
-fun have_common_thm ths1 ths2 =
-  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) (map Meson.make_meta_clause ths2)
+fun have_common_thm ctxt ths1 ths2 =
+  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
+    (map (Meson.make_meta_clause ctxt) ths2)
 
 (*Determining which axiom clauses are actually used*)
 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
@@ -54,14 +55,14 @@
     (if can HOLogic.dest_not t1 then t2 else t1)
     |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
   | _ => raise Fail "expected reflexive or trivial clause")
-  |> Meson.make_meta_clause
+  |> Meson.make_meta_clause ctxt
 
 fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
   let
     val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
     val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
     val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
-  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
+  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause ctxt end
 
 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
   | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
@@ -84,7 +85,7 @@
               (case add_vars_and_frees u [] of
                 [] =>
                 Conv.abs_conv (conv false o snd) ctxt ct
-                |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
+                |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI})
               | v :: _ =>
                 Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
                 |> Thm.cterm_of ctxt
@@ -201,7 +202,7 @@
          val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
          val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
          val (used_th_cls_pairs, unused_th_cls_pairs) =
-           List.partition (have_common_thm used o snd o snd) th_cls_pairs
+           List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
          val unused_ths = maps (snd o snd) unused_th_cls_pairs
          val unused_names = map fst unused_th_cls_pairs
        in
@@ -210,7 +211,7 @@
            verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
          else
            ();
-         if not (null cls) andalso not (have_common_thm used cls) then
+         if not (null cls) andalso not (have_common_thm ctxt used cls) then
            verbose_warning ctxt "The assumptions are inconsistent"
          else
            ();
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -947,7 +947,7 @@
     val U = TFree ("'u", @{sort type})
     val y = Free (yname, U)
     val f' = absdummy (U --> T') (Bound 0 $ y)
-    val th' = Thm.certify_instantiate
+    val th' = Thm.certify_instantiate ctxt
       ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
        [((fst (dest_Var f), (U --> T') --> T'), f')]) th
     val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
@@ -1086,13 +1086,13 @@
               if not (fst (dest_Const pred) = fst (dest_Const pred')) then
                 raise Fail "Trying to instantiate another predicate"
               else ()
-          in Thm.certify_instantiate (subst_of (pred', pred), []) th end
+          in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
         fun instantiate_ho_args th =
           let
             val (_, args') =
               (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
             val ho_args' = map dest_Var (ho_args_of_typ T args')
-          in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+          in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
         val outp_pred =
           Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
         val ((_, ths'), ctxt1) =
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -32,28 +32,28 @@
 
 (* for use when there are no prems to the subgoal *)
 (* does a case split on the given variable *)
-fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
+fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
     let
-      val x = Free(vstr,ty)
+      val thy = Proof_Context.theory_of ctxt;
+
+      val x = Free(vstr,ty);
       val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
 
-      val ctermify = Thm.global_cterm_of sgn;
-      val ctypify = Thm.global_ctyp_of sgn;
-      val case_thm = case_thm_of_ty sgn ty;
+      val case_thm = case_thm_of_ty thy ty;
 
-      val abs_ct = ctermify abst;
-      val free_ct = ctermify x;
+      val abs_ct = Thm.cterm_of ctxt abst;
+      val free_ct = Thm.cterm_of ctxt x;
 
       val (Pv, Dv, type_insts) =
           case (Thm.concl_of case_thm) of
-            (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
+            (_ $ (Pv $ (Dv as Var(D, Dty)))) =>
             (Pv, Dv,
-             Sign.typ_match sgn (Dty, ty) Vartab.empty)
+             Sign.typ_match thy (Dty, ty) Vartab.empty)
           | _ => error "not a valid case thm";
-      val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
+      val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T))
         (Vartab.dest type_insts);
-      val cPv = ctermify (Envir.subst_term_types type_insts Pv);
-      val cDv = ctermify (Envir.subst_term_types type_insts Dv);
+      val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv);
+      val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv);
     in
       Conv.fconv_rule Drule.beta_eta_conversion
          (case_thm
@@ -117,7 +117,6 @@
 fun splitto ctxt splitths genth =
     let
       val _ = not (null splitths) orelse error "splitto: no given splitths";
-      val thy = Thm.theory_of_thm genth;
 
       (* check if we are a member of splitths - FIXME: quicker and
       more flexible with discrim net. *)
@@ -134,7 +133,7 @@
         | SOME v =>
             let
               val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
-              val split_thm = mk_casesplit_goal_thm thy v gt;
+              val split_thm = mk_casesplit_goal_thm ctxt v gt;
               val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
             in
               expf (map recsplitf subthms)
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -7,10 +7,10 @@
 
 signature TFL =
 sig
-  val define_i: bool -> Proof.context -> thm list -> thm list -> xstring -> term -> term list ->
-    theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory
-  val define: bool -> Proof.context -> thm list -> thm list -> xstring -> string -> string list ->
-    theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory
+  val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context ->
+    {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
+  val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
+    {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
   val defer_i: thm list -> xstring -> term list -> theory -> thm * theory
   val defer: thm list -> xstring -> string list -> theory -> thm * theory
 end;
@@ -34,13 +34,13 @@
  * non-proved termination conditions, and finally attempts to prove the
  * simplified termination conditions.
  *--------------------------------------------------------------------------*)
-fun std_postprocessor strict ctxt wfs =
-  Prim.postprocess strict
+fun std_postprocessor ctxt strict wfs =
+  Prim.postprocess ctxt strict
    {wf_tac = REPEAT (ares_tac wfs 1),
     terminator =
       asm_simp_tac ctxt 1
       THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
-        fast_force_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
+        fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
     simplifier = Rules.simpl_conv ctxt []};
 
 
@@ -78,19 +78,21 @@
       val cntxtr = (#1 o USyntax.strip_imp) rhs  (* but union is solider *)
       val cntxt = union (op aconv) cntxtl cntxtr
   in
-    Rules.GEN_ALL
+    Rules.GEN_ALL ctxt
       (Rules.DISCH_ALL
          (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
   end
   val gen_all = USyntax.gen_all
 in
-fun proof_stage strict ctxt wfs theory {f, R, rules, full_pats_TCs, TCs} =
+fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} =
   let
     val _ = writeln "Proving induction theorem ..."
-    val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
+    val ind =
+      Prim.mk_induction (Proof_Context.theory_of ctxt)
+        {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
     val _ = writeln "Postprocessing ...";
     val {rules, induction, nested_tcs} =
-      std_postprocessor strict ctxt wfs theory {rules=rules, induction=ind, TCs=TCs}
+      std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs}
   in
   case nested_tcs
   of [] => {induction=induction, rules=rules,tcs=[]}
@@ -134,29 +136,28 @@
 fun tracing true _ = ()
   | tracing false msg = writeln msg;
 
-fun simplify_defn strict thy ctxt congs wfs id pats def0 =
-   let
-       val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
-       val {rules,rows,TCs,full_pats_TCs} =
-           Prim.post_definition congs thy ctxt (def, pats)
-       val {lhs=f,rhs} = USyntax.dest_eq (concl def)
-       val (_,[R,_]) = USyntax.strip_comb rhs
-       val dummy = Prim.trace_thms ctxt "congs =" congs
-       (*the next step has caused simplifier looping in some cases*)
-       val {induction, rules, tcs} =
-             proof_stage strict ctxt wfs thy
-               {f = f, R = R, rules = rules,
-                full_pats_TCs = full_pats_TCs,
-                TCs = TCs}
-       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
-                        (Rules.CONJUNCTS rules)
-         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
-        rules = ListPair.zip(rules', rows),
-        tcs = (termination_goals rules') @ tcs}
-   end
+fun simplify_defn ctxt strict congs wfs id pats def0 =
+  let
+    val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
+    val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
+    val {lhs=f,rhs} = USyntax.dest_eq (concl def)
+    val (_,[R,_]) = USyntax.strip_comb rhs
+    val dummy = Prim.trace_thms ctxt "congs =" congs
+    (*the next step has caused simplifier looping in some cases*)
+    val {induction, rules, tcs} =
+      proof_stage ctxt strict wfs
+       {f = f, R = R, rules = rules,
+        full_pats_TCs = full_pats_TCs,
+        TCs = TCs}
+    val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
+                      (Rules.CONJUNCTS rules)
+  in
+    {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
+     rules = ListPair.zip(rules', rows),
+     tcs = (termination_goals rules') @ tcs}
+  end
   handle Utils.ERR {mesg,func,module} =>
-               error (mesg ^
-                      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
+    error (mesg ^ "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
 
 
 (* Derive the initial equations from the case-split rules to meet the
@@ -184,21 +185,21 @@
 (*---------------------------------------------------------------------------
  * Defining a function with an associated termination relation.
  *---------------------------------------------------------------------------*)
-fun define_i strict ctxt congs wfs fid R eqs thy =
-  let val {functional,pats} = Prim.mk_functional thy eqs
-      val (thy, def) = Prim.wfrec_definition0 thy fid R functional
-      val ctxt = Proof_Context.transfer thy ctxt
-      val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
-      val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def
-      val rules' = 
-          if strict then derive_init_eqs ctxt rules eqs
-          else rules
-  in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end;
+fun define_i strict congs wfs fid R eqs ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val {functional, pats} = Prim.mk_functional thy eqs
+    val (def, thy') = Prim.wfrec_definition0 fid R functional thy
+    val ctxt' = Proof_Context.transfer thy' ctxt
+    val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
+    val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs fid pats def
+    val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules
+  in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end;
 
-fun define strict ctxt congs wfs fid R seqs thy =
-  define_i strict ctxt congs wfs fid
-      (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) thy
-    handle Utils.ERR {mesg,...} => error mesg;
+fun define strict congs wfs fid R seqs ctxt =
+  define_i strict congs wfs fid
+    (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
+      handle Utils.ERR {mesg,...} => error mesg;
 
 
 (*---------------------------------------------------------------------------
@@ -211,7 +212,8 @@
   #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
 
 fun defer_i congs fid eqs thy =
- let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
+ let
+     val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
      val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
      val dummy = writeln "Proving induction theorem ...";
      val induction = Prim.mk_induction theory
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -21,22 +21,22 @@
   val SPEC: cterm -> thm -> thm
   val ISPEC: cterm -> thm -> thm
   val ISPECL: cterm list -> thm -> thm
-  val GEN: cterm -> thm -> thm
-  val GENL: cterm list -> thm -> thm
+  val GEN: Proof.context -> cterm -> thm -> thm
+  val GENL: Proof.context -> cterm list -> thm -> thm
   val LIST_CONJ: thm list -> thm
 
   val SYM: thm -> thm
   val DISCH_ALL: thm -> thm
   val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
   val SPEC_ALL: thm -> thm
-  val GEN_ALL: thm -> thm
+  val GEN_ALL: Proof.context -> thm -> thm
   val IMP_TRANS: thm -> thm -> thm
   val PROVE_HYP: thm -> thm -> thm
 
   val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
   val EXISTS: cterm * cterm -> thm -> thm
   val EXISTL: cterm list -> thm -> thm
-  val IT_EXISTS: (cterm*cterm) list -> thm -> thm
+  val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
 
   val EVEN_ORS: thm list -> thm list
   val DISJ_CASESL: thm -> thm list -> thm
@@ -47,8 +47,8 @@
 
   val rbeta: thm -> thm
   val tracing: bool Unsynchronized.ref
-  val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
-                             -> thm -> thm * term list
+  val CONTEXT_REWRITE_RULE: Proof.context ->
+    term * term list * thm * thm list -> thm -> thm * term list
   val RIGHT_ASSOC: Proof.context -> thm -> thm
 
   val prove: Proof.context -> bool -> term * tactic -> thm
@@ -158,19 +158,19 @@
 (*----------------------------------------------------------------------------
  *        Disjunction
  *---------------------------------------------------------------------------*)
-local val thy = Thm.theory_of_thm disjI1
-      val prop = Thm.prop_of disjI1
-      val [P,Q] = Misc_Legacy.term_vars prop
-      val disj1 = Thm.forall_intr (Thm.global_cterm_of thy Q) disjI1
+local
+  val prop = Thm.prop_of disjI1
+  val [P,Q] = Misc_Legacy.term_vars prop
+  val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
 in
 fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
   handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
 end;
 
-local val thy = Thm.theory_of_thm disjI2
-      val prop = Thm.prop_of disjI2
-      val [P,Q] = Misc_Legacy.term_vars prop
-      val disj2 = Thm.forall_intr (Thm.global_cterm_of thy P) disjI2
+local
+  val prop = Thm.prop_of disjI2
+  val [P,Q] = Misc_Legacy.term_vars prop
+  val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
 in
 fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
   handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
@@ -262,11 +262,10 @@
  *        Universals
  *---------------------------------------------------------------------------*)
 local (* this is fragile *)
-      val thy = Thm.theory_of_thm spec
-      val prop = Thm.prop_of spec
-      val x = hd (tl (Misc_Legacy.term_vars prop))
-      val cTV = Thm.global_ctyp_of thy (type_of x)
-      val gspec = Thm.forall_intr (Thm.global_cterm_of thy x) spec
+  val prop = Thm.prop_of spec
+  val x = hd (tl (Misc_Legacy.term_vars prop))
+  val cTV = Thm.ctyp_of @{context} (type_of x)
+  val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
 in
 fun SPEC tm thm =
    let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
@@ -279,41 +278,38 @@
 val ISPECL = fold ISPEC;
 
 (* Not optimized! Too complicated. *)
-local val thy = Thm.theory_of_thm allI
-      val prop = Thm.prop_of allI
-      val [P] = Misc_Legacy.add_term_vars (prop, [])
-      fun cty_theta s = map (fn (i, (S, ty)) => (Thm.global_ctyp_of s (TVar (i, S)), Thm.global_ctyp_of s ty))
-      fun ctm_theta s = map (fn (i, (_, tm2)) =>
-                             let val ctm2 = Thm.global_cterm_of s tm2
-                             in (Thm.global_cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
-                             end)
-      fun certify s (ty_theta,tm_theta) =
-        (cty_theta s (Vartab.dest ty_theta),
-         ctm_theta s (Vartab.dest tm_theta))
+local
+  val prop = Thm.prop_of allI
+  val [P] = Misc_Legacy.add_term_vars (prop, [])
+  fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty))
+  fun ctm_theta ctxt =
+    map (fn (i, (_, tm2)) =>
+      let val ctm2 = Thm.cterm_of ctxt tm2
+      in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end)
+  fun certify ctxt (ty_theta,tm_theta) =
+    (cty_theta ctxt (Vartab.dest ty_theta),
+     ctm_theta ctxt (Vartab.dest tm_theta))
 in
-fun GEN v th =
+fun GEN ctxt v th =
    let val gth = Thm.forall_intr v th
-       val thy = Thm.theory_of_thm gth
+       val thy = Proof_Context.theory_of ctxt
        val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
        val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
        val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
-       val allI2 = Drule.instantiate_normalize (certify thy theta) allI
+       val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
        val thm = Thm.implies_elim allI2 gth
        val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
        val prop' = tp $ (A $ Abs(x,ty,M))
-   in ALPHA thm (Thm.global_cterm_of thy prop')
-   end
+   in ALPHA thm (Thm.cterm_of ctxt prop') end
 end;
 
-val GENL = fold_rev GEN;
+fun GENL ctxt = fold_rev (GEN ctxt);
 
-fun GEN_ALL thm =
-   let val thy = Thm.theory_of_thm thm
-       val prop = Thm.prop_of thm
-       val tycheck = Thm.global_cterm_of thy
-       val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
-  in GENL vlist thm
-  end;
+fun GEN_ALL ctxt thm =
+  let
+    val prop = Thm.prop_of thm
+    val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
+  in GENL ctxt vlist thm end;
 
 
 fun MATCH_MP th1 th2 =
@@ -344,24 +340,19 @@
     val t$u = Thm.term_of redex
     val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
   in
-    GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
+    GEN ctxt fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
   end;
 
-local val thy = Thm.theory_of_thm exI
-      val prop = Thm.prop_of exI
-      val [P,x] = Misc_Legacy.term_vars prop
+local
+  val prop = Thm.prop_of exI
+  val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
 in
 fun EXISTS (template,witness) thm =
-   let val thy = Thm.theory_of_thm thm
-       val prop = Thm.prop_of thm
-       val P' = Thm.global_cterm_of thy P
-       val x' = Thm.global_cterm_of thy x
-       val abstr = #2 (Dcterm.dest_comb template)
-   in
-   thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
-     handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
-   end
+  let val abstr = #2 (Dcterm.dest_comb template) in
+    thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
+      handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
+  end
 end;
 
 (*----------------------------------------------------------------------------
@@ -386,16 +377,14 @@
  *---------------------------------------------------------------------------*)
 (* Could be improved, but needs "subst_free" for certified terms *)
 
-fun IT_EXISTS blist th =
-   let val thy = Thm.theory_of_thm th
-       val tych = Thm.global_cterm_of thy
-       val blist' = map (apply2 Thm.term_of) blist
-       fun ex v M  = Thm.global_cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
-
+fun IT_EXISTS ctxt blist th =
+  let
+    val blist' = map (apply2 Thm.term_of) blist
+    fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
   in
-  fold_rev (fn (b as (r1,r2)) => fn thm =>
+    fold_rev (fn (b as (r1,r2)) => fn thm =>
         EXISTS(ex r2 (subst_free [b]
-                   (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)
+                   (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
               thm)
        blist' th
   end;
@@ -509,13 +498,10 @@
 
 (* Note: Thm.rename_params_rule counts from 1, not 0 *)
 fun rename thm =
-  let val thy = Thm.theory_of_thm thm
-      val tych = Thm.global_cterm_of thy
-      val ants = Logic.strip_imp_prems (Thm.prop_of thm)
-      val news = get (ants,1,[])
-  in
-  fold Thm.rename_params_rule news thm
-  end;
+  let
+    val ants = Logic.strip_imp_prems (Thm.prop_of thm)
+    val news = get (ants,1,[])
+  in fold Thm.rename_params_rule news thm end;
 
 
 (*---------------------------------------------------------------------------
@@ -539,8 +525,8 @@
 fun print_thms ctxt s L =
   say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
 
-fun print_cterm ctxt s ct =
-  say (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]);
+fun print_term ctxt s t =
+  say (cat_lines [s, Syntax.string_of_term ctxt t]);
 
 
 (*---------------------------------------------------------------------------
@@ -647,9 +633,9 @@
                             (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
                             t)
 
-fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
+fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
  let val globals = func::G
-     val ctxt0 = empty_simpset (Proof_Context.init_global (Thm.theory_of_thm th))
+     val ctxt0 = empty_simpset main_ctxt
      val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
      val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
      val cut_lemma' = cut_lemma RS eq_reflection
@@ -661,28 +647,28 @@
              val dummy = say "cong rule:"
              val dummy = say (Display.string_of_thm ctxt thm)
              (* Unquantified eliminate *)
-             fun uq_eliminate (thm,imp,thy) =
-                 let val tych = Thm.global_cterm_of thy
-                     val dummy = print_cterm ctxt "To eliminate:" (tych imp)
+             fun uq_eliminate (thm,imp) =
+                 let val tych = Thm.cterm_of ctxt
+                     val _ = print_term ctxt "To eliminate:" imp
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
                      val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
                      val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
                        handle Utils.ERR _ => Thm.reflexive lhs
-                     val dummy = print_thms ctxt' "proven:" [lhs_eq_lhs1]
+                     val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
                   in
                   lhs_eeq_lhs2 COMP thm
                   end
-             fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
+             fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
               let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
                   val dummy = forall (op aconv) (ListPair.zip (vlist, args))
                     orelse error "assertion failed in CONTEXT_REWRITE_RULE"
                   val imp_body1 = subst_free (ListPair.zip (args, vstrl))
                                              imp_body
-                  val tych = Thm.global_cterm_of thy
+                  val tych = Thm.cterm_of ctxt
                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
                   val eq1 = Logic.strip_imp_concl imp_body1
                   val Q = get_lhs eq1
@@ -705,13 +691,13 @@
                   val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
               in ant_th COMP thm
               end
-             fun q_eliminate (thm,imp,thy) =
+             fun q_eliminate (thm, imp) =
               let val (vlist, imp_body, used') = strip_all used imp
                   val (ants,Q) = dest_impl imp_body
               in if (pbeta_redex Q) (length vlist)
-                 then pq_eliminate (thm,thy,vlist,imp_body,Q)
+                 then pq_eliminate (thm, vlist, imp_body, Q)
                  else
-                 let val tych = Thm.global_cterm_of thy
+                 let val tych = Thm.cterm_of ctxt
                      val ants1 = map tych ants
                      val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
                      val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
@@ -725,22 +711,21 @@
               end end
 
              fun eliminate thm =
-               case Thm.prop_of thm
-               of Const(@{const_name Pure.imp},_) $ imp $ _ =>
+               case Thm.prop_of thm of
+                 Const(@{const_name Pure.imp},_) $ imp $ _ =>
                    eliminate
                     (if not(is_all imp)
-                     then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
-                     else q_eliminate (thm, imp, Thm.theory_of_thm thm))
+                     then uq_eliminate (thm, imp)
+                     else q_eliminate (thm, imp))
                             (* Assume that the leading constant is ==,   *)
                 | _ => thm  (* if it is not a ==>                        *)
          in SOME(eliminate (rename thm)) end
          handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
 
         fun restrict_prover ctxt thm =
-          let val dummy = say "restrict_prover:"
+          let val _ = say "restrict_prover:"
               val cntxt = rev (Simplifier.prems_of ctxt)
-              val dummy = print_thms ctxt "cntxt:" cntxt
-              val thy = Thm.theory_of_thm thm
+              val _ = print_thms ctxt "cntxt:" cntxt
               val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
                 Thm.prop_of thm
               fun genl tm = let val vlist = subtract (op aconv) globals
@@ -762,14 +747,13 @@
               val antl = case rcontext of [] => []
                          | _   => [USyntax.list_mk_conj(map cncl rcontext)]
               val TC = genl(USyntax.list_mk_imp(antl, A))
-              val dummy = print_cterm ctxt "func:" (Thm.global_cterm_of thy func)
-              val dummy = print_cterm ctxt "TC:" (Thm.global_cterm_of thy (HOLogic.mk_Trueprop TC))
-              val dummy = tc_list := (TC :: !tc_list)
+              val _ = print_term ctxt "func:" func
+              val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
+              val _ = tc_list := (TC :: !tc_list)
               val nestedp = is_some (USyntax.find_term is_func TC)
-              val dummy = if nestedp then say "nested" else say "not_nested"
+              val _ = if nestedp then say "nested" else say "not_nested"
               val th' = if nestedp then raise RULES_ERR "solver" "nested function"
-                        else let val cTC = Thm.global_cterm_of thy
-                                              (HOLogic.mk_Trueprop TC)
+                        else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
                              in case rcontext of
                                 [] => SPEC_ALL(ASSUME cTC)
                                | _ => MP (SPEC_ALL (ASSUME cTC))
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -11,8 +11,8 @@
   val trace_cterm: Proof.context -> string -> cterm -> unit
   type pattern
   val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
-  val wfrec_definition0: theory -> string -> term -> term -> theory * thm
-  val post_definition: thm list -> theory -> Proof.context -> thm * pattern list ->
+  val wfrec_definition0: string -> term -> term -> theory -> thm * theory
+  val post_definition: Proof.context -> thm list -> thm * pattern list ->
    {rules: thm,
     rows: int list,
     TCs: term list list,
@@ -32,9 +32,10 @@
     patterns : pattern list}
   val mk_induction: theory ->
     {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
-  val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm}
-    -> theory -> {rules: thm, induction: thm, TCs: term list list}
-    -> {rules: thm, induction: thm, nested_tcs: thm list}
+  val postprocess: Proof.context -> bool ->
+    {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
+    {rules: thm, induction: thm, TCs: term list list} ->
+    {rules: thm, induction: thm, nested_tcs: thm list}
 end;
 
 structure Prim: PRIM =
@@ -364,21 +365,23 @@
   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
 
-local val f_eq_wfrec_R_M =
-           #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
-      val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
-      val (fname,_) = dest_Free f
-      val (wfrec,_) = USyntax.strip_comb rhs
+local
+  val f_eq_wfrec_R_M =
+    #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
+  val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
+  val (fname,_) = dest_Free f
+  val (wfrec,_) = USyntax.strip_comb rhs
 in
-fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
- let val def_name = Thm.def_name (Long_Name.base_name fid)
-     val wfrec_R_M =  map_types poly_tvars
-                          (wfrec $ map_types poly_tvars R)
-                      $ functional
-     val def_term = const_def thy (fid, Ty, wfrec_R_M)
-     val ([def], thy') =
+
+fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
+  let
+    val def_name = Thm.def_name (Long_Name.base_name fid)
+    val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
+    val def_term = const_def thy (fid, Ty, wfrec_R_M)
+    val ([def], thy') =
       Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
- in (thy', def) end;
+  in (def, thy') end;
+
 end;
 
 
@@ -415,8 +418,9 @@
 
 fun givens pats = map pat_of (filter given pats);
 
-fun post_definition meta_tflCongs theory ctxt (def, pats) =
- let val tych = Thry.typecheck theory
+fun post_definition ctxt meta_tflCongs (def, pats) =
+ let val thy = Proof_Context.theory_of ctxt
+     val tych = Thry.typecheck thy
      val f = #lhs(USyntax.dest_eq(concl def))
      val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
      val pats' = filter given pats
@@ -425,9 +429,8 @@
      val WFR = #ant(USyntax.dest_imp(concl corollary))
      val R = #Rand(USyntax.dest_comb WFR)
      val corollary' = Rules.UNDISCH corollary  (* put WF R on assums *)
-     val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary')
-                           given_pats
-     val (case_rewrites,context_congs) = extraction_thms theory
+     val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
+     val (case_rewrites,context_congs) = extraction_thms thy
      (*case_ss causes minimal simplification: bodies of case expressions are
        not simplified. Otherwise large examples (Red-Black trees) are too
        slow.*)
@@ -435,10 +438,10 @@
        put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
-              (Symtab.dest (BNF_LFP_Compat.get_all theory [BNF_LFP_Compat.Keep_Nesting]))
+              (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
-     val extract = Rules.CONTEXT_REWRITE_RULE
-                     (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
+     val extract =
+      Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
      val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
      val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
@@ -495,8 +498,8 @@
      val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
      val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
      val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries
-     fun extract X = Rules.CONTEXT_REWRITE_RULE
-                       (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
+     val extract =
+      Rules.CONTEXT_REWRITE_RULE ctxt (f, R1::SV, @{thm cut_apply}, tflCongs @ context_congs)
  in {proto_def = proto_def,
      SV=SV,
      WFR=WFR,
@@ -535,30 +538,30 @@
      val (c,args) = USyntax.strip_comb lhs
      val (name,Ty) = dest_atom c
      val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
-     val ([def0], theory) =
+     val ([def0], thy') =
        thy
        |> Global_Theory.add_defs false
             [Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
      val def = Thm.unvarify_global def0;
+     val ctxt' = Syntax.init_pretty_global thy';
      val dummy =
-       if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
+       if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def)
        else ()
      (* val fconst = #lhs(USyntax.dest_eq(concl def))  *)
-     val tych = Thry.typecheck theory
+     val tych = Thry.typecheck thy'
      val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
          (*lcp: a lot of object-logic inference to remove*)
      val baz = Rules.DISCH_ALL
                  (fold_rev Rules.DISCH full_rqt_prop
                   (Rules.LIST_CONJ extractants))
-     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
-                           else ()
+     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else ()
      val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
      val SV' = map tych SV;
      val SVrefls = map Thm.reflexive SV'
      val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
                    SVrefls def)
                 RS meta_eq_to_obj_eq
-     val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0
+     val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN ctxt' (tych R1) baz)) def0
      val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
      val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
                        theory Hilbert_Choice*)
@@ -566,7 +569,7 @@
          handle ERROR msg => cat_error msg
     "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
      val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
- in {theory = theory, R=R1, SV=SV,
+ in {theory = thy', R=R1, SV=SV,
      rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def',
      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
      patterns = pats}
@@ -633,7 +636,7 @@
  fun fail s = raise TFL_ERR "mk_case" s
  fun mk{rows=[],...} = fail"no rows"
    | mk{path=[], rows = [([], (thm, bindings))]} =
-                         Rules.IT_EXISTS (map tych_binding bindings) thm
+                         Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
    | mk{path = u::rstp, rows as (p::_, _)::_} =
      let val (pat_rectangle,rights) = ListPair.unzip rows
          val col0 = map hd pat_rectangle
@@ -693,7 +696,7 @@
      val th0 = Rules.ASSUME (tych a_eq_v)
      val rows = map (fn x => ([x], (th0,[]))) pats
  in
- Rules.GEN (tych a)
+ Rules.GEN ctxt (tych a)
        (Rules.RIGHT_ASSOC ctxt
           (Rules.CHOOSE ctxt (tych v, ex_th0)
                 (mk_case ty_info (vname::aname::names)
@@ -774,14 +777,14 @@
  *           TCs = TC_1[pat] ... TC_n[pat]
  *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
  *---------------------------------------------------------------------------*)
-fun prove_case f thy (tm,TCs_locals,thm) =
- let val tych = Thry.typecheck thy
+fun prove_case ctxt f (tm,TCs_locals,thm) =
+ let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
      val antc = tych(#ant(USyntax.dest_imp tm))
      val thm' = Rules.SPEC_ALL thm
      fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
      fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
      fun mk_ih ((TC,locals),th2,nested) =
-         Rules.GENL (map tych locals)
+         Rules.GENL ctxt (map tych locals)
             (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
              else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
              else Rules.MP th2 TC)
@@ -845,7 +848,7 @@
     val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
     val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
-    val proved_cases = map (prove_case fconst thy) tasks
+    val proved_cases = map (prove_case ctxt fconst) tasks
     val v =
       Free (singleton
         (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
@@ -855,14 +858,14 @@
     val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
                           (substs, proved_cases)
     val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
-    val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
+    val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
     val dc = Rules.MP Sinduct dant
     val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
     val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
-    val dc' = fold_rev (Rules.GEN o tych) vars
+    val dc' = fold_rev (Rules.GEN ctxt o tych) vars
                        (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
 in
-   Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
+   Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
 end
 handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
 
@@ -911,14 +914,15 @@
   else ();
 
 
-fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
-let val ctxt = Proof_Context.init_global theory;
-    val tych = Thry.typecheck theory;
+fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val tych = Thry.typecheck thy;
 
    (*---------------------------------------------------------------------
     * Attempt to eliminate WF condition. It's the only assumption of rules
     *---------------------------------------------------------------------*)
-   val (rules1,induction1)  =
+    val (rules1,induction1)  =
        let val thm =
         Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
        in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
@@ -947,7 +951,7 @@
                  (r,ind)
          handle Utils.ERR _ =>
           (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
-           simplify_induction theory tc_eq ind))
+           simplify_induction thy tc_eq ind))
        end
 
    (*----------------------------------------------------------------------
@@ -966,7 +970,7 @@
    fun simplify_nested_tc tc =
       let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
       in
-      Rules.GEN_ALL
+      Rules.GEN_ALL ctxt
        (Rules.MATCH_MP Thms.eqT tc_eq
         handle Utils.ERR _ =>
           (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -697,7 +697,7 @@
     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     val thm2 = thm1
-      |> Thm.certify_instantiate (instT, [])
+      |> Thm.certify_instantiate ctxt (instT, [])
       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
@@ -733,7 +733,7 @@
     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     val thm2 = thm1
-      |> Thm.certify_instantiate (instT, [])
+      |> Thm.certify_instantiate ctxt (instT, [])
       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -140,7 +140,7 @@
             val cT = Thm.ctyp_of_cterm cv
             val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
           in thm RS spec' end
-        fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm
+        fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
         fun process_single ((name, atts), rew_imp, frees) args =
           let
             fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm
@@ -152,7 +152,7 @@
                 Global_Theory.store_thm (Binding.name name, thm) thy)
           in
             swap args
-            |> apfst (remove_alls frees)
+            |> remove_alls frees
             |> apfst undo_imps
             |> apfst Drule.export_without_context
             |-> Thm.theory_attributes
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -65,7 +65,7 @@
   val partition_rules: thm -> thm list -> (string * thm list) list
   val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
   val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
-  val infer_intro_vars: thm -> int -> thm list -> term list list
+  val infer_intro_vars: theory -> thm -> int -> thm list -> term list list
 end;
 
 signature INDUCTIVE =
@@ -1132,9 +1132,8 @@
     (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
 
 (* infer order of variables in intro rules from order of quantifiers in elim rule *)
-fun infer_intro_vars elim arity intros =
+fun infer_intro_vars thy elim arity intros =
   let
-    val thy = Thm.theory_of_thm elim;
     val _ :: cases = Thm.prems_of elim;
     val used = map (fst o fst) (Term.add_vars (Thm.prop_of elim) []);
     fun mtch (t, u) =
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -19,9 +19,9 @@
     [name] => name
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
-fun prf_of thm =
+fun prf_of thy thm =
   Reconstruct.proof_of thm
-  |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)];  (* FIXME *)
+  |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]
   | subsets (x::xs) =
@@ -268,7 +268,7 @@
     if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
     Extraction.abs_corr_shyps thy rule vs vs2
       (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
-         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
+         (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
   end;
 
 fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
@@ -285,7 +285,7 @@
     val params' = map dest_Var params;
     val rss = Inductive.partition_rules raw_induct intrs;
     val rss' = map (fn (((s, rs), (_, arity)), elim) =>
-      (s, (Inductive.infer_intro_vars elim arity rs ~~ rs)))
+      (s, (Inductive.infer_intro_vars thy elim arity rs ~~ rs)))
         (rss ~~ arities ~~ elims);
     val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/recdef.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -85,7 +85,7 @@
 
 type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
 
-structure GlobalRecdefData = Theory_Data
+structure Data = Generic_Data
 (
   type T = recdef_info Symtab.table * hints;
   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
@@ -99,28 +99,15 @@
           Thm.merge_thms (wfs1, wfs2)));
 );
 
-val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
-
-fun put_recdef name info thy =
-  let
-    val (tab, hints) = GlobalRecdefData.get thy;
-    val tab' = Symtab.update_new (name, info) tab
-      handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
-  in GlobalRecdefData.put (tab', hints) thy end;
-
-val get_global_hints = #2 o GlobalRecdefData.get;
+val get_recdef = Symtab.lookup o #1 o Data.get o Context.Theory;
 
-
-(* proof data *)
+fun put_recdef name info =
+  (Context.theory_map o Data.map o apfst) (fn tab =>
+    Symtab.update_new (name, info) tab
+      handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name));
 
-structure LocalRecdefData = Proof_Data
-(
-  type T = hints;
-  val init = get_global_hints;
-);
-
-val get_hints = LocalRecdefData.get;
-fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
+val get_hints = #2 o Data.get o Context.Proof;
+val map_hints = Data.map o apsnd;
 
 
 (* attributes *)
@@ -155,25 +142,23 @@
 
 
 
-(** prepare_hints(_i) **)
+(** prepare hints **)
 
-fun prepare_hints thy opt_src =
+fun prepare_hints opt_src ctxt =
   let
-    val ctxt0 = Proof_Context.init_global thy;
-    val ctxt =
+    val ctxt' =
       (case opt_src of
-        NONE => ctxt0
-      | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0));
+        NONE => ctxt
+      | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt));
+    val {simps, congs, wfs} = get_hints ctxt';
+    val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong};
+  in ((rev (map snd congs), wfs), ctxt'') end;
+
+fun prepare_hints_i () ctxt =
+  let
     val {simps, congs, wfs} = get_hints ctxt;
     val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
-  in (ctxt', rev (map snd congs), wfs) end;
-
-fun prepare_hints_i thy () =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val {simps, congs, wfs} = get_global_hints thy;
-    val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
-  in (ctxt', rev (map snd congs), wfs) end;
+  in ((rev (map snd congs), wfs), ctxt') end;
 
 
 
@@ -190,30 +175,30 @@
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
 
-    val (ctxt, congs, wfs) = prep_hints thy hints;
+    val ((congs, wfs), ctxt) = prep_hints hints (Proof_Context.init_global thy);
     (*We must remove imp_cong to prevent looping when the induction rule
       is simplified. Many induction rules have nested implications that would
       give rise to looping conditional rewriting.*)
-    val ({lhs, rules = rules_idx, induct, tcs}, thy) =
-      tfl_fn not_permissive ctxt congs wfs name R eqs thy;
+    val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) =
+      tfl_fn not_permissive congs wfs name R eqs ctxt;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
       if null tcs then [Simplifier.simp_add,
         Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
       else [];
-    val ((simps' :: rules', [induct']), thy) =
-      thy
+    val ((simps' :: rules', [induct']), thy2) =
+      Proof_Context.theory_of ctxt1
       |> Sign.add_path bname
       |> Global_Theory.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
       ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
-    val thy =
-      thy
+    val thy3 =
+      thy2
       |> put_recdef name result
       |> Sign.parent_path;
-  in (thy, result) end;
+  in (thy3, result) end;
 
 val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
 fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
diff -r 2e1c1968b38e -r d3f561aa2af6 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/split_rule.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -39,12 +39,11 @@
   | ap_split _ T3 u = u;
 
 (*Curries any Var of function type in the rule*)
-fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
+fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
       let val T' = HOLogic.flatten_tupleT T1 ---> T2;
           val newt = ap_split T1 T2 (Var (v, T'));
-          val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
-      in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
-  | split_rule_var' _ rl = rl;
+      in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end
+  | split_rule_var' _ _ rl = rl;
 
 
 (* complete splitting of partially split rules *)
@@ -54,9 +53,8 @@
         (incr_boundvars 1 u) $ Bound 0))
   | ap_split' _ _ u = u;
 
-fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
+fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) =
       let
-        val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
         val (Us', U') = strip_type T;
         val Us = take (length ts) Us';
         val U = drop (length ts) Us' ---> U';
@@ -65,17 +63,19 @@
               let
                 val Ts = HOLogic.flatten_tupleT T;
                 val ys = Name.variant_list xs (replicate (length Ts) a);
-              in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
-                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
+              in
+                (xs @ ys,
+                  apply2 (Thm.cterm_of ctxt)
+                    (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
+                      (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts)
               end
           | mk_tuple _ x = x;
         val newt = ap_split' Us U (Var (v, T'));
-        val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
         val (vs', insts) = fold mk_tuple ts (vs, []);
       in
-        (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+        (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs')
       end
-  | complete_split_rule_var _ x = x;
+  | complete_split_rule_var _ _ x = x;
 
 fun collect_vars (Abs (_, _, t)) = collect_vars t
   | collect_vars t =
@@ -85,11 +85,11 @@
 
 
 fun split_rule_var ctxt =
-  (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var';
+  (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt;
 
 (*curries ALL function variables occurring in a rule's conclusion*)
 fun split_rule ctxt rl =
-  fold_rev split_rule_var' (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
+  fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
   |> remove_internal_split ctxt
   |> Drule.export_without_context;
 
@@ -100,7 +100,7 @@
     val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
     val vars = collect_vars prop [];
   in
-    fst (fold_rev complete_split_rule_var vars (rl, xs))
+    fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs))
     |> remove_internal_split ctxt
     |> Drule.export_without_context
     |> Rule_Cases.save rl
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Provers/clasimp.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -63,27 +63,26 @@
   Failing other cases, A is added as a Safe Intr rule*)
 
 fun add_iff safe unsafe =
-  Thm.declaration_attribute (fn th =>
+  Thm.declaration_attribute (fn th => fn context =>
     let
       val n = Thm.nprems_of th;
       val (elim, intro) = if n = 0 then safe else unsafe;
       val zero_rotate = zero_var_indexes o rotate_prems n;
-    in
-      Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #>
-      Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
-      handle THM _ =>
-        (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE))
-          handle THM _ => Thm.attribute_declaration intro th)
-    end);
+      val decls =
+        [(intro, zero_rotate (th RS Data.iffD2)),
+         (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
+        handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
+        handle THM _ => [(intro, th)];
+    in fold (uncurry Thm.attribute_declaration) decls context end);
 
-fun del_iff del = Thm.declaration_attribute (fn th =>
-  let val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th) in
-    Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #>
-    Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
-    handle THM _ =>
-      (Thm.attribute_declaration del (zero_rotate (th RS Data.notE))
-        handle THM _ => Thm.attribute_declaration del th)
-  end);
+fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
+  let
+    val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
+    val rls =
+      [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
+        handle THM _ => [zero_rotate (th RS Data.notE)]
+        handle THM _ => [th];
+  in fold (Thm.attribute_declaration del) rls context end);
 
 in
 
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Provers/splitter.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -285,9 +285,8 @@
    call split_posns with appropriate parameters
 *************************************************************)
 
-fun select cmap state i =
+fun select thy cmap state i =
   let
-    val thy = Thm.theory_of_thm state
     val goal = Thm.term_of (Thm.cprem_of state i);
     val Ts = rev (map #2 (Logic.strip_params goal));
     val _ $ t $ _ = Logic.strip_assums_concl goal;
@@ -313,16 +312,14 @@
    i       : no. of subgoal
 **************************************************************)
 
-fun inst_lift Ts t (T, U, pos) state i =
+fun inst_lift ctxt Ts t (T, U, pos) state i =
   let
-    val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
     val (cntxt, u) = mk_cntxt t pos (T --> U);
     val trlift' = Thm.lift_rule (Thm.cprem_of state i)
       (Thm.rename_boundvars abs_lift u trlift);
     val (P, _) = strip_comb (fst (Logic.dest_equals
       (Logic.strip_assums_concl (Thm.prop_of trlift'))));
-  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] trlift'
-  end;
+  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end;
 
 
 (*************************************************************
@@ -338,15 +335,13 @@
    i     : number of subgoal
 **************************************************************)
 
-fun inst_split Ts t tt thm TB state i =
+fun inst_split ctxt Ts t tt thm TB state i =
   let
     val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
     val (P, _) = strip_comb (fst (Logic.dest_equals
       (Logic.strip_assums_concl (Thm.prop_of thm'))));
-    val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
     val cntxt = mk_cntxt_splitthm t tt TB;
-  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
-  end;
+  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end;
 
 
 (*****************************************************************************
@@ -359,14 +354,15 @@
 fun split_tac _ [] i = no_tac
   | split_tac ctxt splits i =
   let val cmap = cmap_of_split_thms splits
-      fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st
+      fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift ctxt Ts t p st i, 2) i st
       fun lift_split_tac state =
-            let val (Ts, t, splits) = select cmap state i
+            let val (Ts, t, splits) = select (Proof_Context.theory_of ctxt) cmap state i
             in case splits of
                  [] => no_tac state
                | (thm, apsns, pos, TB, tt)::_ =>
                    (case apsns of
-                      [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state
+                      [] =>
+                        compose_tac ctxt (false, inst_split ctxt Ts t tt thm TB state i, 0) i state
                     | p::_ => EVERY [lift_tac Ts t p,
                                      resolve_tac ctxt [reflexive_thm] (i+1),
                                      lift_split_tac] state)
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/Isar/code.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -635,19 +635,19 @@
     else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
   end;
 
-fun desymbolize_tvars thms =
+fun desymbolize_tvars thy thms =
   let
     val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
     val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
-  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
+  in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end;
 
-fun desymbolize_vars thm =
+fun desymbolize_vars thy thm =
   let
     val vs = Term.add_vars (Thm.prop_of thm) [];
     val var_subst = mk_desymbolization I I Var vs;
-  in Thm.certify_instantiate ([], var_subst) thm end;
+  in Thm.global_certify_instantiate thy ([], var_subst) thm end;
 
-fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
+fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
 
 
 (* abstype certificates *)
@@ -706,7 +706,7 @@
   in
     thm
     |> Thm.varifyT_global
-    |> Thm.certify_instantiate (inst, [])
+    |> Thm.global_certify_instantiate thy (inst, [])
     |> pair subst
   end;
 
@@ -771,7 +771,7 @@
         val sorts = map_transpose inter_sorts vss;
         val vts = Name.invent_names Name.context Name.aT sorts;
         val thms' =
-          map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
+          map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms;
         val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
         fun head_conv ct = if can Thm.dest_comb ct
           then Conv.fun_conv head_conv ct
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -935,7 +935,7 @@
 
 fun comp_hhf_tac ctxt th i st =
   PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
-    (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
+    (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
 
 fun comp_incr_tac _ [] _ = no_tac
   | comp_incr_tac ctxt (th :: ths) i =
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/drule.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -17,7 +17,7 @@
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
   val gen_all: int -> thm -> thm
-  val lift_all: cterm -> thm -> thm
+  val lift_all: Proof.context -> cterm -> thm -> thm
   val implies_elim_list: thm -> thm list -> thm
   val implies_intr_list: cterm list -> thm -> thm
   val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -192,9 +192,12 @@
 
 (*lift vars wrt. outermost goal parameters
   -- reverses the effect of gen_all modulo higher-order unification*)
-fun lift_all goal th =
+fun lift_all ctxt raw_goal raw_th =
   let
-    val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
+    val thy = Proof_Context.theory_of ctxt;
+    val goal = Thm.transfer_cterm thy raw_goal;
+    val th = Thm.transfer thy raw_th;
+
     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));
@@ -204,8 +207,8 @@
       |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
   in
     th
-    |> Thm.instantiate (Thm.certify_inst thy ([], inst))
-    |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
+    |> Thm.certify_instantiate ctxt ([], inst)
+    |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
   end;
 
 (*direct generalization*)
@@ -225,10 +228,8 @@
   | zero_var_indexes_list ths =
       let
         val thy = Theory.merge_list (map Thm.theory_of_thm ths);
-        val inst =
-          Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
-          |> Thm.certify_inst thy;
-      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
+        val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+      in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
 
@@ -359,7 +360,7 @@
   Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
 
 fun store_standard_thm name th = store_thm name (export_without_context th);
-fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
+fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);
 
 val reflexive_thm =
   let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/more_thm.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -60,10 +60,15 @@
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
-  val certify_inst: theory ->
+  val global_certify_inst: theory ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     (ctyp * ctyp) list * (cterm * cterm) list
-  val certify_instantiate:
+  val global_certify_instantiate: theory ->
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+  val certify_inst: Proof.context ->
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+    (ctyp * ctyp) list * (cterm * cterm) list
+  val certify_instantiate: Proof.context ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
   val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
@@ -351,12 +356,19 @@
 
 (* certify_instantiate *)
 
-fun certify_inst thy (instT, inst) =
+fun global_certify_inst thy (instT, inst) =
  (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
   map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
 
-fun certify_instantiate insts th =
-  Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+fun global_certify_instantiate thy insts th =
+  Thm.instantiate (global_certify_inst thy insts) th;
+
+fun certify_inst ctxt (instT, inst) =
+ (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
+  map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
+
+fun certify_instantiate ctxt insts th =
+  Thm.instantiate (certify_inst ctxt insts) th;
 
 
 (* forall_intr_frees: generalization over all suitable Free variables *)
@@ -375,6 +387,8 @@
 
 fun unvarify_global th =
   let
+    val thy = Thm.theory_of_thm th;
+
     val prop = Thm.full_prop_of th;
     val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
@@ -383,7 +397,7 @@
     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
       let val T' = Term_Subst.instantiateT instT T
       in (((a, i), T'), Free ((a, T'))) end);
-  in certify_instantiate (instT, inst) th end;
+  in global_certify_instantiate thy (instT, inst) th end;
 
 
 (* close_derivation *)
@@ -444,7 +458,7 @@
     val _ = Sign.no_vars ctxt prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
-    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.global_ctyp_of thy T, S)) strip;
+    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip;
 
     val thy' = thy
       |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
@@ -461,7 +475,7 @@
 fun add_def ctxt unchecked overloaded (b, prop) thy =
   let
     val _ = Sign.no_vars ctxt prop;
-    val prems = map (Thm.global_cterm_of thy) (Logic.strip_imp_prems prop);
+    val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
 
     val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/subgoal.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -31,7 +31,9 @@
 
 fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   let
-    val st = Simplifier.norm_hhf_protect ctxt raw_st;
+    val st = raw_st
+      |> Thm.transfer (Proof_Context.theory_of ctxt)
+      |> Simplifier.norm_hhf_protect ctxt;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
 
@@ -40,9 +42,8 @@
       else ([], goal);
     val text = asms @ (if do_concl then [concl] else []);
 
-    val ((_, schematic_terms), ctxt3) =
-      Variable.import_inst true (map Thm.term_of text) ctxt2
-      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
 
     val schematics = (schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/variable.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -578,9 +578,8 @@
 
 fun importT ths ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+    val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
     val ths' = map (Thm.instantiate insts') ths;
   in ((instT', ths'), ctxt') end;
 
@@ -592,9 +591,8 @@
 
 fun import is_open ths ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val insts' = Thm.certify_inst thy insts;
+    val insts' = Thm.certify_inst ctxt' insts;
     val ths' = map (Thm.instantiate insts') ths;
   in ((insts', ths'), ctxt') end;
 
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -178,7 +178,7 @@
     if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
     then (I, ct)
     else
-     (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
+     (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
       Thm.cterm_of ctxt (map_types normalize t))
   end;
 
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/IsaPlanner/isand.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -137,14 +137,12 @@
  ["SG0", ..., "SGm"] : thm list ->   -- export function
    "G" : thm)
 *)
-fun subgoal_thms th =
+fun subgoal_thms ctxt th =
   let
-    val thy = Thm.theory_of_thm th;
-
     val t = Thm.prop_of th;
 
     val prems = Logic.strip_imp_prems t;
-    val aprems = map (Thm.trivial o Thm.global_cterm_of thy) prems;
+    val aprems = map (Thm.trivial o Thm.cterm_of ctxt) prems;
 
     fun explortf premths = Drule.implies_elim_list th premths;
   in (aprems, explortf) end;
@@ -167,7 +165,7 @@
 (* requires being given solutions! *)
 fun fixed_subgoal_thms ctxt th =
   let
-    val (subgoals, expf) = subgoal_thms th;
+    val (subgoals, expf) = subgoal_thms ctxt th;
 (*  fun export_sg (th, exp) = exp th; *)
     fun export_sgs expfs solthms =
       expf (map2 (curry (op |>)) solthms expfs);
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -30,15 +30,13 @@
 th: A vs ==> B vs
 Results in: "B vs" [!!x. A x]
 *)
-fun allify_conditions Ts th =
+fun allify_conditions ctxt Ts th =
   let
-    val thy = Thm.theory_of_thm th;
-
     fun allify (x, T) t =
       Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
 
-    val cTs = map (Thm.global_cterm_of thy o Free) Ts;
-    val cterm_asms = map (Thm.global_cterm_of thy o fold_rev allify Ts) (Thm.prems_of th);
+    val cTs = map (Thm.cterm_of ctxt o Free) Ts;
+    val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th);
     val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
   in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
 
@@ -82,7 +80,7 @@
       |> Drule.forall_elim_list tonames;
 
     (* make unconditional rule and prems *)
-    val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
+    val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule';
 
     (* using these names create lambda-abstracted version of the rule *)
     val abstractions = rev (Ts' ~~ tonames);
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/eqsubst.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -14,7 +14,7 @@
     * term (* outer term *)
 
   type searchinfo =
-    theory
+    Proof.context
     * int (* maxidx *)
     * Zipper.T (* focusterm to search under *)
 
@@ -67,7 +67,7 @@
   * term; (* outer term *)
 
 type searchinfo =
-  theory
+  Proof.context
   * int (* maxidx *)
   * Zipper.T; (* focusterm to search under *)
 
@@ -138,8 +138,8 @@
   end;
 
 (* Unification with exception handled *)
-(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
-fun clean_unify thy ix (a as (pat, tgt)) =
+(* given context, max var index, pat, tgt; returns Seq of instantiations *)
+fun clean_unify ctxt ix (a as (pat, tgt)) =
   let
     (* type info will be re-derived, maybe this can be cached
        for efficiency? *)
@@ -148,7 +148,7 @@
     (* FIXME is it OK to ignore the type instantiation info?
        or should I be using it? *)
     val typs_unify =
-      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
+      SOME (Sign.typ_unify (Proof_Context.theory_of ctxt) (pat_ty, tgt_ty) (Vartab.empty, ix))
         handle Type.TUNIFY => NONE;
   in
     (case typs_unify of
@@ -161,7 +161,7 @@
              Vartab.dest (Envir.term_env env));
           val initenv =
             Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
-          val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv
+          val useq = Unify.smash_unifiers (Context.Proof ctxt) [a] initenv
             handle ListPair.UnequalLengths => Seq.empty
               | Term.TERM _ => Seq.empty;
           fun clean_unify' useq () =
@@ -181,10 +181,10 @@
    bound variables. New names have been introduced to make sure they are
    unique w.r.t all names in the term and each other. usednames' is
    oldnames + new names. *)
-fun clean_unify_z thy maxidx pat z =
+fun clean_unify_z ctxt maxidx pat z =
   let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
     Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
-      (clean_unify thy maxidx (t, pat))
+      (clean_unify ctxt maxidx (t, pat))
   end;
 
 
@@ -230,8 +230,8 @@
       end;
   in Zipper.lzy_search sf_valid_td_lr end;
 
-fun searchf_unify_gen f (thy, maxidx, z) lhs =
-  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
+fun searchf_unify_gen f (ctxt, maxidx, z) lhs =
+  Seq.map (clean_unify_z ctxt maxidx lhs) (Zipper.limit_apply f z);
 
 (* search all unifications *)
 val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
@@ -271,7 +271,7 @@
        o Zipper.mktop
        o Thm.prop_of) conclthm
   in
-    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
+    ((cfvs, conclthm), (ctxt, maxidx, ft))
   end;
 
 (* substitute using an object or meta level equality *)
@@ -345,23 +345,20 @@
     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 asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
     val asm_nprems = length (Logic.strip_imp_prems asmt);
 
-    val pth = Thm.trivial (cert asmt);
+    val pth = Thm.trivial ((Thm.cterm_of ctxt) asmt);
     val maxidx = Thm.maxidx_of th;
 
     val ft =
       (Zipper.move_down_right (* trueprop *)
          o Zipper.mktop
          o Thm.prop_of) pth
-  in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end;
+  in ((cfvs, j, asm_nprems, pth), (ctxt, maxidx, ft)) end;
 
 (* prepare subst in every possible assumption *)
 fun prep_subst_in_asms ctxt i gth =
diff -r 2e1c1968b38e -r d3f561aa2af6 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/misc_legacy.ML	Wed Jun 03 21:48:40 2015 +0200
@@ -23,8 +23,8 @@
   val mk_defpair: term * term -> string * term
   val get_def: theory -> xstring -> thm
   val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic
-  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
-  val freeze_thaw: thm -> thm * (thm -> thm)
+  val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm)
+  val freeze_thaw: Proof.context -> thm -> thm * (thm -> thm)
 end;
 
 structure Misc_Legacy: MISC_LEGACY =
@@ -161,13 +161,12 @@
 fun metahyps_aux_tac ctxt tacf (prem,gno) state =
   let val (insts,params,hyps,concl) = metahyps_split_prem prem
       val maxidx = Thm.maxidx_of state
-      val cterm = Thm.global_cterm_of (Thm.theory_of_thm state)
-      val chyps = map cterm hyps
+      val chyps = map (Thm.cterm_of ctxt) hyps
       val hypths = map Thm.assume chyps
       val subprems = map (Thm.forall_elim_vars 0) hypths
       val fparams = map Free params
-      val cparams = map cterm fparams
-      fun swap_ctpair (t,u) = (cterm u, cterm t)
+      val cparams = map (Thm.cterm_of ctxt) fparams
+      fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t)
       (*Subgoal variables: make Free; lift type over params*)
       fun mk_subgoal_inst concl_vars (v, T) =
           if member (op =) concl_vars (v, T)
@@ -175,12 +174,12 @@
           else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
       (*Instantiate subgoal vars by Free applied to params*)
       fun mk_ctpair (v, in_concl, u) =
-          if in_concl then (cterm (Var v), cterm u)
-          else (cterm (Var v), cterm (list_comb (u, fparams)))
+          if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u)
+          else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams))
       (*Restore Vars with higher type and index*)
       fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
-          if in_concl then (cterm u, cterm (Var ((a, i), T)))
-          else (cterm u, cterm (Var ((a, i + maxidx), U)))
+          if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T))
+          else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U))
       (*Embed B in the original context of params and hyps*)
       fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
       (*Strip the context using elimination rules*)
@@ -193,7 +192,7 @@
             and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
             val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
             val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
-            val emBs = map (cterm o embed) (Thm.prems_of st')
+            val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
             val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
         in  (*restore the unknowns to the hypotheses*)
             free_instantiate (map swap_ctpair insts @
@@ -206,7 +205,7 @@
       fun next st =
         Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
           (false, relift st, Thm.nprems_of st) gno state
-  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
+  in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end;
 
 fun print_vars_terms ctxt n thm =
   let
@@ -255,9 +254,8 @@
 (*Convert all Vars in a theorem to Frees.  Also return a function for
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
 
-fun freeze_thaw_robust th =
+fun freeze_thaw_robust ctxt th =
  let val fth = Thm.legacy_freezeT th
-     val thy = Thm.theory_of_thm fth
  in
    case Thm.fold_terms Term.add_vars fth [] of
        [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
@@ -265,8 +263,8 @@
          let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
              val alist = map newName vars
              fun mk_inst (v,T) =
-                 (Thm.global_cterm_of thy (Var(v,T)),
-                  Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
+                 apply2 (Thm.cterm_of ctxt)
+                  (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
              val insts = map mk_inst vars
              fun thaw i th' = (*i is non-negative increment for Var indexes*)
                  th' |> forall_intr_list (map #2 insts)
@@ -276,9 +274,8 @@
 
 (*Basic version of the function above. No option to rename Vars apart in thaw.
   The Frees created from Vars have nice names.*)
-fun freeze_thaw th =
+fun freeze_thaw ctxt th =
  let val fth = Thm.legacy_freezeT th
-     val thy = Thm.theory_of_thm fth
  in
    case Thm.fold_terms Term.add_vars fth [] of
        [] => (fth, fn x => x)
@@ -289,8 +286,7 @@
              val (alist, _) =
                  fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
              fun mk_inst (v, T) =
-                 (Thm.global_cterm_of thy (Var(v,T)),
-                  Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
+                apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
              val insts = map mk_inst vars
              fun thaw th' =
                  th' |> forall_intr_list (map #2 insts)
@@ -299,4 +295,3 @@
  end;
 
 end;
-