# HG changeset patch
# User blanchet
# Date 1387080706 -3600
# Node ID 283fc522d24e8045bbc8b92112fef45cf861f0e9
# Parent  7068557b7c6313b59f3e5718f5abb7663a6a4b95# Parent  b9ae4a2f615b06fbab6557a74a08bea644c823d4
merge

diff -r 7068557b7c63 -r 283fc522d24e NEWS
--- a/NEWS	Sat Dec 14 07:45:30 2013 +0800
+++ b/NEWS	Sun Dec 15 05:11:46 2013 +0100
@@ -115,6 +115,11 @@
 Note that 'ML_file' is the canonical command to load ML files into the
 formal context.
 
+* Proper context for basic Simplifier operations: rewrite_rule,
+rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
+pass runtime Proof.context (and ensure that the simplified entity
+actually belongs to it).
+
 
 *** System ***
 
diff -r 7068557b7c63 -r 283fc522d24e src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/CCL/CCL.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -280,7 +280,7 @@
     fun mk_dstnct_thm rls s =
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
         (fn _ =>
-          rewrite_goals_tac defs THEN
+          rewrite_goals_tac ctxt defs THEN
           simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
   in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
 
diff -r 7068557b7c63 -r 283fc522d24e src/Doc/IsarImplementation/Eq.thy
--- a/src/Doc/IsarImplementation/Eq.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Doc/IsarImplementation/Eq.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -91,30 +91,30 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\
-  @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\
-  @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
-  @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
-  @{index_ML fold_goals_tac: "thm list -> tactic"} \\
+  @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
+  @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
+  @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
+  @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole
+  \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
   theorem by the given rules.
 
-  \item @{ML rewrite_goals_rule}~@{text "rules thm"} rewrites the
+  \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
   outer premises of the given theorem.  Interpreting the same as a
   goal state (\secref{sec:tactical-goals}) it means to rewrite all
   subgoals (in the same manner as @{ML rewrite_goals_tac}).
 
-  \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
+  \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
   @{text "i"} by the given rewrite rules.
 
-  \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals
+  \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
   by the given rewrite rules.
 
-  \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML
+  \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
   rewrite_goals_tac} with the symmetric form of each member of @{text
   "rules"}, re-ordered to fold longer expression first.  This supports
   to idea to fold primitive definitions that appear in expended form
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -590,10 +590,10 @@
       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
     val expand_rels =
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
-    val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
-    val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
-    val unfold_rels = unfold_thms lthy rel_unfolds;
-    val unfold_all = unfold_sets o unfold_maps o unfold_rels;
+    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
+    fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
+    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
+    fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
     val bnf_sets = map (expand_maps o expand_sets)
       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
@@ -627,7 +627,7 @@
       map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
 
     fun mk_tac thm {context = ctxt, prems = _} =
-      (rtac (unfold_all thm) THEN'
+      (rtac (unfold_all ctxt thm) THEN'
       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
 
     val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
@@ -638,7 +638,8 @@
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
+    fun wit_tac {context = ctxt, prems = _} =
+      mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
 
     val (bnf', lthy') =
       bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -130,7 +130,7 @@
       REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
     EVERY [REPEAT_DETERM_N r
         (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
-      if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
+      if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
       mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
   end;
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -168,7 +168,7 @@
             cterm_instantiate_pos cts rel_xtor_co_induct_thm
             |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
             |> funpow (2 * n) (fn thm => thm RS spec)
-            |> Conv.fconv_rule Object_Logic.atomize
+            |> Conv.fconv_rule (Object_Logic.atomize lthy)
             |> funpow n (fn thm => thm RS mp)
           end);
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -567,7 +567,7 @@
       EVERY' [rtac allI, fo_rtac induct ctxt,
         select_prem_tac n (dtac @{thm meta_spec2}) i,
         REPEAT_DETERM_N n o
-          EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac,
+          EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
             REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac],
         atac];
   in
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -45,7 +45,7 @@
     rtac (Drule.instantiate_normalize insts thm) 1
   end);
 
-fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
+fun mk_unfold_thms_then_tac ctxt defs tac x = unfold_thms_tac ctxt defs THEN tac x;
 
 (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
 fun mk_pointfree ctxt thm = thm
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Bali/Example.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -894,7 +894,7 @@
 
 declare member_is_static_simp [simp]
 declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
+ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
 lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
 
@@ -1189,7 +1189,7 @@
 
 ML {* bind_thms ("eval_intros", map 
         (simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o 
-         rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
+         rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
 
 axiomatization
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -2920,7 +2920,7 @@
 struct
 
 fun tactic ctxt alternative T ps = 
-  Object_Logic.full_atomize_tac
+  Object_Logic.full_atomize_tac ctxt
   THEN' CSUBGOAL (fn (g, i) =>
     let
       val th = frpar_oracle (ctxt, alternative, T, ps, g)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -62,7 +62,7 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
+fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
   let
     val thy = Proof_Context.theory_of ctxt
     (* Transform the term*)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -66,7 +66,7 @@
 
 
 fun linr_tac ctxt q =
-    Object_Logic.atomize_prems_tac
+    Object_Logic.atomize_prems_tac ctxt
         THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
         THEN' SUBGOAL (fn (g, i) =>
   let
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -224,7 +224,7 @@
   (case dlo_instance ctxt p of
     NONE => no_tac
   | SOME instance =>
-      Object_Logic.full_atomize_tac i THEN
+      Object_Logic.full_atomize_tac ctxt i THEN
       simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
       CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
       simp_tac ctxt i));  (* FIXME really? *)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -237,11 +237,11 @@
   (case dlo_instance ctxt p of
     (ss, NONE) => simp_tac (put_simpset ss ctxt) i
   | (ss, SOME instance) =>
-      Object_Logic.full_atomize_tac i THEN
+      Object_Logic.full_atomize_tac ctxt i THEN
       simp_tac (put_simpset ss ctxt) i
       THEN (CONVERSION Thm.eta_long_conversion) i
       THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
-      THEN Object_Logic.full_atomize_tac i
+      THEN Object_Logic.full_atomize_tac ctxt i
       THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
       THEN (simp_tac (put_simpset ss ctxt) i)));
 end;
\ No newline at end of file
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -82,7 +82,7 @@
 
 
 fun mir_tac ctxt q = 
-    Object_Logic.atomize_prems_tac
+    Object_Logic.atomize_prems_tac ctxt
         THEN' simp_tac (put_simpset HOL_basic_ss ctxt
           addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
         THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOL.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -1496,8 +1496,9 @@
                     | is_conj _ = false
                 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
               | _ => NONE))]
-    |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
-      map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
+    |> Simplifier.set_mksimps (fn ctxt =>
+        Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
+        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
 *}
 
 text {* Pre-simplification of induction and cases rules *}
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -208,29 +208,29 @@
   txt {* 10 - 7 *}
   apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
   txt {* 6 *}
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
 
   txt {* 6 - 5 *}
   apply (tactic "EVERY1 [tac2,tac2]")
 
   txt {* 4 *}
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   apply (tactic "tac2 1")
 
   txt {* 3 *}
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
 
   apply (tactic "tac2 1")
-  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
+  apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
     (@{thm Impl.hdr_sum_def})] *})
   apply arith
 
   txt {* 2 *}
   apply (tactic "tac2 1")
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   apply (intro strip)
   apply (erule conjE)+
@@ -238,11 +238,12 @@
 
   txt {* 1 *}
   apply (tactic "tac2 1")
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   apply (intro strip)
   apply (erule conjE)+
-  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic {* fold_goals_tac @{context}
+    [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   apply simp
 
   done
@@ -286,13 +287,13 @@
   apply (intro strip, (erule conjE)+)
   apply (rule imp_disjL [THEN iffD1])
   apply (rule impI)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
     (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   apply simp
   apply (erule conjE)+
   apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
     k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm inv1_def}]
                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   apply (simp add: hdr_sum_def Multiset.count_def)
   apply (rule add_le_mono)
@@ -307,7 +308,7 @@
   apply (intro strip, (erule conjE)+)
   apply (rule imp_disjL [THEN iffD1])
   apply (rule impI)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
     (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   apply simp
   done
@@ -333,7 +334,7 @@
   txt {* 2 b *}
 
   apply (intro strip, (erule conjE)+)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
                                (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   apply simp
 
@@ -341,9 +342,9 @@
   apply (tactic "tac4 1")
   apply (intro strip, (erule conjE)+)
   apply (rule ccontr)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
                                (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
                                (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
   apply simp
   apply (erule_tac x = "m" in allE)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -101,8 +101,8 @@
     : thm =
   let
     fun tac {prems, context} =
-      rewrite_goals_tac defs THEN
-      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
+      rewrite_goals_tac context defs THEN
+      EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
   in
     Goal.prove_global thy [] [] goal tac
   end
@@ -213,8 +213,10 @@
           in (n2, mk_ssumT (t1, t2)) end
       val ct = ctyp_of thy (snd (cons2typ 1 spec'))
       val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
-      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
-      val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2
+      val thm2 = rewrite_rule (Proof_Context.init_global thy)
+        (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
+      val thm3 = rewrite_rule (Proof_Context.init_global thy)
+        [mk_meta_eq @{thm conj_assoc}] thm2
 
       val y = Free ("y", lhsT)
       fun one_con (con, args) =
@@ -225,15 +227,15 @@
         in Library.foldr mk_ex (vs, conj) end
       val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
       (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
-      val tacs = [
+      fun tacs {context = ctxt, prems} = [
           rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
-          rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
+          rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
           rtac thm3 1]
     in
-      val nchotomy = prove thy con_betas goal (K tacs)
+      val nchotomy = prove thy con_betas goal tacs
       val exhaust =
           (nchotomy RS @{thm exh_casedist0})
-          |> rewrite_rule @{thms exh_casedists}
+          |> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
           |> Drule.zero_var_indexes
     end
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -161,12 +161,12 @@
               val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules)
               fun arg_tac (lazy, _) =
                   rtac (if lazy then allI else case_UU_allI) 1
-              val tacs =
-                  rewrite_goals_tac @{thms atomize_all atomize_imp} ::
+              fun tacs ctxt =
+                  rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} ::
                   map arg_tac args @
                   [REPEAT (rtac impI 1), ALLGOALS simplify]
             in
-              Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
+              Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context)
             end
           fun eq_thms (p, cons) = map (con_thm p) cons
           val conss = map #con_specs constr_infos
@@ -321,7 +321,7 @@
       val rules = @{thm Rep_cfun_strict1} :: take_0_thms
       fun tacf {prems, context = ctxt} =
         let
-          val prem' = rewrite_rule [bisim_def_thm] (hd prems)
+          val prem' = rewrite_rule ctxt [bisim_def_thm] (hd prems)
           val prems' = Project_Rule.projections ctxt prem'
           val dests = map (fn th => th RS spec RS spec RS mp) prems'
           fun one_tac (dest, rews) =
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -157,10 +157,10 @@
     (* prove applied version of definitions *)
     fun prove_proj (lhs, rhs) =
       let
-        val tac = rewrite_goals_tac fixdef_thms THEN
+        fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
           (simp_tac (Simplifier.global_context thy beta_ss)) 1
         val goal = Logic.mk_equals (lhs, rhs)
-      in Goal.prove_global thy [] [] goal (K tac) end
+      in Goal.prove_global thy [] [] goal (tac o #context) end
     val proj_thms = map prove_proj projs
 
     (* mk_tuple lhss == fixpoint *)
@@ -328,7 +328,7 @@
       in
         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
          EVERY
-          [rewrite_goals_tac map_apply_thms,
+          [rewrite_goals_tac ctxt map_apply_thms,
            rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
            REPEAT (resolve_tac adm_rules 1),
            simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
@@ -533,11 +533,11 @@
       let
         val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
         val DEFL_simps = RepData.get (Proof_Context.init_global thy)
-        val tac =
-          rewrite_goals_tac (map mk_meta_eq DEFL_simps)
+        fun tac ctxt =
+          rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
           THEN TRY (resolve_tac defl_unfold_thms 1)
       in
-        Goal.prove_global thy [] [] goal (K tac)
+        Goal.prove_global thy [] [] goal (tac o #context)
       end
     val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns
 
@@ -641,7 +641,7 @@
       in
         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
          EVERY
-          [rewrite_goals_tac (defl_apply_thms @ map_apply_thms),
+          [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
            rtac (@{thm cont_parallel_fix_ind}
              OF [defl_cont_thm, map_cont_thm]) 1,
            REPEAT (resolve_tac adm_rules 1),
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -470,15 +470,15 @@
     fun prove_finite_thm (absT, finite_const) =
       let
         val goal = mk_trp (finite_const $ Free ("x", absT))
-        val tac =
+        fun tac ctxt =
             EVERY [
-            rewrite_goals_tac finite_defs,
+            rewrite_goals_tac ctxt finite_defs,
             rtac @{thm lub_ID_finite} 1,
             resolve_tac chain_take_thms 1,
             resolve_tac lub_take_thms 1,
             resolve_tac decisive_thms 1]
       in
-        Goal.prove_global thy [] [] goal (K tac)
+        Goal.prove_global thy [] [] goal (tac o #context)
       end
     val finite_thms =
         map prove_finite_thm (absTs ~~ finite_consts)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -411,8 +411,8 @@
     : thm =
   let
     fun tac {prems, context} =
-      rewrite_goals_tac defs THEN
-      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
+      rewrite_goals_tac context defs THEN
+      EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
   in
     Goal.prove_global thy [] [] goal tac
   end;
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Library/State_Monad.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -145,7 +145,7 @@
   "_sdo_block (_sdo_final e)" => "e"
 
 text {*
-  For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
+  For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman.thy"}.
 *}
 
 end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -938,7 +938,7 @@
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
 fun sos_tac print_cert prover ctxt =
-  Object_Logic.full_atomize_tac THEN'
+  Object_Logic.full_atomize_tac ctxt THEN'
   elim_denom_tac ctxt THEN'
   core_sos_tac print_cert prover ctxt;
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -325,7 +325,7 @@
   apply(  fast intro: hext_trans)
 
 
-apply( tactic prune_params_tac)
+apply( tactic "prune_params_tac @{context}")
 -- "Level 52"
 
 -- "1 Call"
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -399,7 +399,7 @@
 
  fun norm_arith_tac ctxt =
    clarify_tac (put_claset HOL_cs ctxt) THEN'
-   Object_Logic.full_atomize_tac THEN'
+   Object_Logic.full_atomize_tac ctxt THEN'
    CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
 
 end;
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/NSA/transfer.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -58,11 +58,11 @@
     val meta = Local_Defs.meta_rewrite_rule ctxt;
     val ths' = map meta ths;
     val unfolds' = map meta unfolds and refolds' = map meta refolds;
-    val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t))
+    val (_$_$t') = concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (cterm_of thy t))
     val u = unstar_term consts t'
     val tac =
-      rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
-      ALLGOALS Object_Logic.full_atomize_tac THEN
+      rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
+      ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
       match_tac [transitive_thm] 1 THEN
       resolve_tac [@{thm transfer_start}] 1 THEN
       REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
@@ -76,7 +76,7 @@
               val tr = transfer_thm_of ctxt ths t
               val (_$l$r) = concl_of tr;
               val trs = if l aconv r then [] else [tr];
-            in rewrite_goals_tac trs th end))
+            in rewrite_goals_tac ctxt trs th end))
 
 local
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nat.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -1536,19 +1536,19 @@
 
 simproc_setup nateq_cancel_sums
   ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
-  {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
+  {* fn phi => try o Nat_Arith.cancel_eq_conv *}
 
 simproc_setup natless_cancel_sums
   ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
-  {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
+  {* fn phi => try o Nat_Arith.cancel_less_conv *}
 
 simproc_setup natle_cancel_sums
   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
-  {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
+  {* fn phi => try o Nat_Arith.cancel_le_conv *}
 
 simproc_setup natdiff_cancel_sums
   ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
-  {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
+  {* fn phi => try o Nat_Arith.cancel_diff_conv *}
 
 ML_file "Tools/lin_arith.ML"
 setup {* Lin_Arith.global_setup *}
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -829,6 +829,7 @@
        (* instantiations.                                                 *)
        val (_, thy33) =
          let
+             val ctxt32 = Proof_Context.init_global thy32;
 
              (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
              (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
@@ -918,7 +919,7 @@
             ||>> add_thmss_string
               let
                 val thms1 = inst_pt_at [all_eqvt];
-                val thms2 = map (fold_rule [inductive_forall_def]) thms1
+                val thms2 = map (fold_rule ctxt32 [inductive_forall_def]) thms1
               in
                 [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
               end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -134,7 +134,7 @@
 val at_fin_set_fresh = @{thm at_fin_set_fresh};
 val abs_fun_eq1 = @{thm abs_fun_eq1};
 
-val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
+fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
 
 fun mk_perm Ts t u =
   let
@@ -595,10 +595,12 @@
         end))
         (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
 
+    val ctxt6 = Proof_Context.init_global thy6;
+
     val perm_defs = map snd typedefs;
-    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
+    val Abs_inverse_thms = map (collect_simp ctxt6 o #Abs_inverse o snd o fst) typedefs;
     val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
-    val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
+    val Rep_thms = map (collect_simp ctxt6 o #Rep o snd o fst) typedefs;
 
 
     (** prove that new types are in class pt_<name> **)
@@ -616,7 +618,7 @@
             (Sign.intern_type thy name,
               map (inter_sort thy sort o snd) tvs, [pt_class])
             (fn ctxt => EVERY [Class.intro_classes_tac [],
-              rewrite_goals_tac [perm_def],
+              rewrite_goals_tac ctxt [perm_def],
               asm_full_simp_tac (ctxt addsimps [Rep_inverse]) 1,
               asm_full_simp_tac (ctxt addsimps
                 [Rep RS perm_closed RS Abs_inverse]) 1,
@@ -645,7 +647,7 @@
             (Sign.intern_type thy name,
               map (inter_sort thy sort o snd) tvs, [cp_class])
             (fn ctxt => EVERY [Class.intro_classes_tac [],
-              rewrite_goals_tac [perm_def],
+              rewrite_goals_tac ctxt [perm_def],
               asm_full_simp_tac (ctxt addsimps
                 ((Rep RS perm_closed1 RS Abs_inverse) ::
                  (if atom1 = atom2 then []
@@ -783,7 +785,7 @@
         new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
       (thy7, [], [], []);
 
-    val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
+    val abs_inject_thms = map (collect_simp ctxt6 o #Abs_inject o snd o fst) typedefs
     val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
 
     (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
@@ -792,9 +794,9 @@
       let
         val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
         val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
-      in Goal.prove_global_future thy8 [] [] eqn (fn _ => EVERY
+      in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY
         [resolve_tac inj_thms 1,
-         rewrite_goals_tac rewrites,
+         rewrite_goals_tac ctxt rewrites,
          rtac refl 3,
          resolve_tac rep_intrs 2,
          REPEAT (resolve_tac Rep_thms 1)])
@@ -1043,7 +1045,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn {prems, context = ctxt} => EVERY
         [rtac indrule_lemma' 1,
-         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms' 1),
             simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
@@ -2017,8 +2019,8 @@
         Goal.prove_global_future thy12 []
           (map (augment_sort thy12 fs_cp_sort) prems')
           (augment_sort thy12 fs_cp_sort concl')
-          (fn {prems, ...} => EVERY
-            [rewrite_goals_tac reccomb_defs,
+          (fn {context = ctxt, prems} => EVERY
+            [rewrite_goals_tac ctxt reccomb_defs,
              rtac @{thm the1_equality} 1,
              solve rec_unique_thms prems 1,
              resolve_tac rec_intrs 1,
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -87,7 +87,7 @@
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
+    val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
 
     val finish_rule =
       split_all_tuples defs_ctxt
@@ -101,7 +101,7 @@
     (fn i => fn st =>
       rules
       |> inst_mutual_rule ctxt insts avoiding
-      |> Rule_Cases.consume (flat defs) facts
+      |> Rule_Cases.consume ctxt (flat defs) facts
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
@@ -118,10 +118,10 @@
                  else
                    Induct.arbitrary_tac defs_ctxt k xs)
             end)
-          THEN' Induct.inner_atomize_tac) j))
-        THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
+          THEN' Induct.inner_atomize_tac defs_ctxt) j))
+        THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' =>
             Induct.guess_instance ctxt
-              (finish_rule (Induct.internalize more_consumes rule)) i st'
+              (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
                 (rtac (rename_params_rule false [] rule') i THEN
@@ -129,7 +129,7 @@
     THEN_ALL_NEW_CASES
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
         else K all_tac)
-       THEN_ALL_NEW Induct.rulify_tac)
+       THEN_ALL_NEW Induct.rulify_tac ctxt)
   end;
 
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -373,8 +373,8 @@
           |> snd
         end)
       [goals] |>
-    Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
-      rewrite_goals_tac defs_thms THEN
+    Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
+      rewrite_goals_tac ctxt defs_thms THEN
       compose_tac (false, rule, length rule_prems) 1))) |>
     Seq.hd
   end;
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Action.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -108,23 +108,26 @@
    "world" parameter of the form (s,t) and apply additional rewrites.
 *)
 
-fun action_unlift th =
-  (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))
-    handle THM _ => int_unlift th;
+fun action_unlift ctxt th =
+  (rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
+    handle THM _ => int_unlift ctxt th;
 
 (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
 val action_rewrite = int_rewrite
 
-fun action_use th =
+fun action_use ctxt th =
     case (concl_of th) of
       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
-              (flatten (action_unlift th) handle THM _ => th)
+              (flatten (action_unlift ctxt th) handle THM _ => th)
     | _ => th;
 *}
 
-attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
-attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
-attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
+attribute_setup action_unlift =
+  {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
+attribute_setup action_rewrite =
+  {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
+attribute_setup action_use =
+  {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
 
 
 (* =========================== square / angle brackets =========================== *)
@@ -258,11 +261,11 @@
    should plug in only "very safe" rules that can be applied blindly.
    Note that it applies whatever simplifications are currently active.
 *)
-fun action_simp_tac ss intros elims =
+fun action_simp_tac ctxt intros elims =
     asm_full_simp_tac
-         (ss setloop (fn _ => (resolve_tac ((map action_use intros)
+         (ctxt setloop (fn _ => (resolve_tac ((map (action_use ctxt) intros)
                                     @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
-                      ORELSE' (eresolve_tac ((map action_use elims)
+                      ORELSE' (eresolve_tac ((map (action_use ctxt) elims)
                                              @ [conjE,disjE,exE]))));
 *}
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Intensional.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -243,12 +243,12 @@
    |- F --> G  becomes   F w --> G w
 *)
 
-fun int_unlift th =
-  rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
+fun int_unlift ctxt th =
+  rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
 
 (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
-fun int_rewrite th =
-  zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
+fun int_rewrite ctxt th =
+  zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
 
 (* flattening turns "-->" into "==>" and eliminates conjunctions in the
    antecedent. For example,
@@ -282,17 +282,20 @@
     hflatten t
   end
 
-fun int_use th =
+fun int_use ctxt th =
     case (concl_of th) of
       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
-              (flatten (int_unlift th) handle THM _ => th)
+              (flatten (int_unlift ctxt th) handle THM _ => th)
     | _ => th
 *}
 
-attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
-attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
+attribute_setup int_unlift =
+  {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
+attribute_setup int_rewrite =
+  {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
 attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
-attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
+attribute_setup int_use =
+  {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
 
 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   by (simp add: Valid_def)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Memory/Memory.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -223,11 +223,11 @@
   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   apply (case_tac "arg (ch w p)")
    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Read_def},
-     temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
+     temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
    apply (force dest: base_pair [temp_use])
   apply (erule contrapos_np)
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Write_def},
-    temp_rewrite @{thm enabled_ex}])
+    temp_rewrite @{context} @{thm enabled_ex}])
     [@{thm WriteInner_enabled}, exI] [] 1 *})
   done
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -233,7 +233,7 @@
 
 setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
 
-ML {* val temp_elim = make_elim o temp_use *}
+ML {* val temp_elim = make_elim oo temp_use *}
 
 
 
@@ -352,7 +352,7 @@
          --> unchanged (rmhist!p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
     @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
-    @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
+    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
 
 
 (* ------------------------------ State S2 ---------------------------------------- *)
@@ -566,7 +566,8 @@
          & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
          --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-      (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
+      (map (temp_elim @{context})
+        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
    using [[fast_solver]]
    apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
   done
@@ -576,7 +577,8 @@
          --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
              & unchanged (e p, r p, m p, rmhist!p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
+    (map (temp_elim @{context})
+      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
    using [[fast_solver]]
    apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
   done
@@ -586,9 +588,10 @@
          --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
              | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
+    (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   apply (tactic {* action_simp_tac @{context} []
-    (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
+    (@{thm squareE} ::
+      map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
    apply (auto dest!: S3Hist [temp_use])
   done
 
@@ -599,9 +602,10 @@
              | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
              | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
+    (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
-    (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
+    (@{thm squareE} ::
+      map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
   apply (auto dest!: S4Hist [temp_use])
   done
 
@@ -610,8 +614,8 @@
          --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
              | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
-  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
+    (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
+  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
    using [[fast_solver]]
    apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
   done
@@ -621,9 +625,9 @@
          --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
              | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
+    (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   apply (tactic {* action_simp_tac @{context} []
-    (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
+    (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
      apply (auto dest: S6Hist [temp_use])
   done
 
@@ -795,8 +799,8 @@
   SELECT_GOAL
    (TRY (rtac @{thm actionI} 1) THEN
     Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
-    rewrite_goals_tac @{thms action_rews} THEN
-    forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
+    rewrite_goals_tac ctxt @{thms action_rews} THEN
+    forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
     asm_full_simp_tac ctxt 1);
 *}
 
@@ -898,7 +902,7 @@
 lemma S1_RNextdisabled: "|- S1 rmhist p -->
          ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
-    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
+    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
   apply force
   done
 
@@ -1103,7 +1107,7 @@
    apply (erule InfiniteEnsures)
     apply assumption
    apply (tactic {* action_simp_tac @{context} []
-     (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
+     (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
   apply (auto simp: SF_def)
   apply (erule contrapos_np)
   apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
@@ -1190,7 +1194,7 @@
       ==> sigma |= []<>S1 rmhist p"
   apply (rule classical)
   apply (tactic {* asm_lr_simp_tac (@{context} addsimps
-    [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
+    [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
   apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
   done
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/TLA.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -118,25 +118,30 @@
    functions defined in theory Intensional in that they introduce a
    "world" parameter of type "behavior".
 *)
-fun temp_unlift th =
-  (rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th;
+fun temp_unlift ctxt th =
+  (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
+    handle THM _ => action_unlift ctxt th;
 
 (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
 val temp_rewrite = int_rewrite
 
-fun temp_use th =
+fun temp_use ctxt th =
   case (concl_of th) of
     Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
-            ((flatten (temp_unlift th)) handle THM _ => th)
+            ((flatten (temp_unlift ctxt th)) handle THM _ => th)
   | _ => th;
 
-fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
+fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
 *}
 
-attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *}
-attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *}
-attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *}
-attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
+attribute_setup temp_unlift =
+  {* Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of)) *}
+attribute_setup temp_rewrite =
+  {* Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of)) *}
+attribute_setup temp_use =
+  {* Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of)) *}
+attribute_setup try_rewrite =
+  {* Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of)) *}
 
 
 (* ------------------------------------------------------------------------- *)
@@ -584,7 +589,7 @@
     (EVERY
      [auto_tac ctxt,
       TRY (merge_box_tac 1),
-      rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
+      rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *)
       TRYALL (etac @{thm Stable})]);
 
 (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -40,7 +40,7 @@
   in
     thms
     |> Conjunction.intr_balanced
-    |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
+    |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
     |> Thm.implies_intr assum
     |> Thm.generalize ([], params) 0
     |> Axclass.unoverload thy
@@ -94,14 +94,14 @@
         (def, lthy')
       end;
 
-    fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
+    fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
 
     val qualify =
       Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
   in
     Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
     #> add_def
-    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
+    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
     #-> fold Code.del_eqn
     #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
     #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -32,8 +32,6 @@
 val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
-val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
-
 fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
   #exhaust (the (Symtab.lookup dt_info tname));
 
@@ -271,6 +269,8 @@
 
     val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
 
+    val collect_simp = rewrite_rule (Proof_Context.init_global thy4) [mk_meta_eq mem_Collect_eq];
+
     val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) =>
       (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep));
 
@@ -355,7 +355,7 @@
         val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
         val char_thms' =
           map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
-            (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
+            (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac refl 1])) eqns;
 
       in (thy', char_thms' @ char_thms) end;
 
@@ -418,13 +418,13 @@
           Goal.prove_sorry_global thy5 [] []
             (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
             (fn {context = ctxt, ...} => EVERY
-              [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+              [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
                REPEAT (EVERY
                  [rtac allI 1, rtac impI 1,
                   Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
                   REPEAT (EVERY
                     [hyp_subst_tac ctxt 1,
-                     rewrite_goals_tac rewrites,
+                     rewrite_goals_tac ctxt rewrites,
                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
                      (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
                      ORELSE (EVERY
@@ -443,9 +443,10 @@
         val elem_thm =
           Goal.prove_sorry_global thy5 [] []
             (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
-            (fn _ =>
-              EVERY [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
-                rewrite_goals_tac rewrites,
+            (fn {context = ctxt, ...} =>
+              EVERY [
+                (Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
+                rewrite_goals_tac ctxt rewrites,
                 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
                   ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
 
@@ -480,11 +481,11 @@
       else
         drop (length newTs) (Datatype_Aux.split_conj_thm
           (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
-             [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+             [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
               REPEAT (rtac TrueI 1),
-              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
+              rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} ::
                 Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
-              rewrite_goals_tac (map Thm.symmetric range_eqs),
+              rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
               REPEAT (EVERY
                 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
                    maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
@@ -511,9 +512,9 @@
         val rewrites = @{thm o_def} :: constr_defs @ map (mk_meta_eq o #2) newT_iso_axms;
       in
         Goal.prove_sorry_global thy5 [] [] eqn
-        (fn _ => EVERY
+        (fn {context = ctxt, ...} => EVERY
           [resolve_tac inj_thms 1,
-           rewrite_goals_tac rewrites,
+           rewrite_goals_tac ctxt rewrites,
            rtac refl 3,
            resolve_tac rep_intrs 2,
            REPEAT (resolve_tac iso_elem_thms 1)])
@@ -634,7 +635,7 @@
       (fn {context = ctxt, prems, ...} =>
         EVERY
           [rtac indrule_lemma' 1,
-           (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+           (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
            EVERY (map (fn (prem, r) => (EVERY
              [REPEAT (eresolve_tac Abs_inverse_thms 1),
               simp_tac (put_simpset HOL_basic_ss ctxt
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -27,6 +27,9 @@
 
 fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
   let
+    val ctxt = Proof_Context.init_global thy;
+    val cert = cterm_of thy;
+
     val recTs = Datatype_Aux.get_rec_types descr;
     val pnames =
       if length descr = 1 then ["P"]
@@ -104,7 +107,6 @@
         (map (fn ((((i, _), T), U), tname) =>
           make_pred i U T (mk_proj i is r) (Free (tname, T)))
             (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
-    val cert = cterm_of thy;
     val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
       (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
 
@@ -112,10 +114,10 @@
       Goal.prove_internal (map cert prems) (cert concl)
         (fn prems =>
            EVERY [
-            rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
+            rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
             rtac (cterm_instantiate inst induct) 1,
-            ALLGOALS Object_Logic.atomize_prems_tac,
-            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
+            ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
+            rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
             REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
               REPEAT (etac allE i) THEN atac i)) 1)])
       |> Drule.export_without_context;
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Datatype/primrec.ML
--- a/src/HOL/Tools/Datatype/primrec.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/primrec.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -245,8 +245,10 @@
       let
         val frees = fold (Variable.add_free_names ctxt) eqs [];
         val rewrites = rec_rewrites' @ map (snd o snd) defs;
-        fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
-      in map (fn eq => Goal.prove ctxt frees [] eq tac) eqs end;
+      in
+        map (fn eq => Goal.prove ctxt frees [] eq
+          (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
+      end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -207,8 +207,8 @@
           (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts))
           (fn {context = ctxt, ...} =>
             #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
-              (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
-                  rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
+              (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
+                  rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
       end;
 
     val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
@@ -247,8 +247,8 @@
     val rec_thms =
       map (fn t =>
         Goal.prove_sorry_global thy2 [] [] t
-          (fn _ => EVERY
-            [rewrite_goals_tac reccomb_defs,
+          (fn {context = ctxt, ...} => EVERY
+            [rewrite_goals_tac ctxt reccomb_defs,
              rtac @{thm the1_equality} 1,
              resolve_tac rec_unique_thms 1,
              resolve_tac rec_intrs 1,
@@ -327,8 +327,8 @@
     val case_thms =
       (map o map) (fn t =>
           Goal.prove_sorry_global thy2 [] [] t
-            (fn _ =>
-              EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
+            (fn {context = ctxt, ...} =>
+              EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
         (Datatype_Prop.make_cases case_names descr thy2);
   in
     thy2
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/function_lib.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -107,12 +107,14 @@
 
 fun regroup_conv neu cn ac is ct =
  let
+   val thy = theory_of_cterm ct
+   val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
+
    val mk = HOLogic.mk_binop cn
    val t = term_of ct
    val xs = dest_binop_list cn t
    val js = subtract (op =) is (0 upto (length xs) - 1)
    val ty = fastype_of t
-   val thy = theory_of_cterm ct
  in
    Goal.prove_internal []
      (cterm_of thy
@@ -122,7 +124,7 @@
           else if null js
             then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
             else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
-     (K (rewrite_goals_tac ac
+     (K (rewrite_goals_tac ctxt ac
          THEN rtac Drule.reflexive_thm 1))
  end
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -38,12 +38,12 @@
   branches: scheme_branch list,
   cases: scheme_case list}
 
-val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
-val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
+fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize}
+fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify}
 
 fun meta thm = thm RS eq_reflection
 
-val sum_prod_conv = Raw_Simplifier.rewrite true
+fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
   (map meta (@{thm split_conv} :: @{thms sum.cases}))
 
 fun term_conv thy cv t =
@@ -187,13 +187,15 @@
   end
 
 
-fun mk_ind_goal thy branches =
+fun mk_ind_goal ctxt branches =
   let
+    val thy = Proof_Context.theory_of ctxt
+
     fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
       HOLogic.mk_Trueprop (list_comb (P, map Free xs))
       |> fold_rev (curry Logic.mk_implies) Cs
       |> fold_rev (Logic.all o Free) ws
-      |> term_conv thy ind_atomize
+      |> term_conv thy (ind_atomize ctxt)
       |> Object_Logic.drop_judgment thy
       |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in
@@ -203,6 +205,9 @@
 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
   (IndScheme {T, cases=scases, branches}) =
   let
+    val thy = Proof_Context.theory_of ctxt
+    val cert = cterm_of thy
+
     val n = length branches
     val scases_idx = map_index I scases
 
@@ -210,10 +215,7 @@
       SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
     val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
 
-    val thy = Proof_Context.theory_of ctxt
-    val cert = cterm_of thy
-
-    val P_comp = mk_ind_goal thy branches
+    val P_comp = mk_ind_goal ctxt branches
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
     val ihyp = Logic.all_const T $ Abs ("z", T,
@@ -270,8 +272,8 @@
                 sih
                 |> Thm.forall_elim (cert (inject idx rcargs))
                 |> Thm.elim_implies (import ineq) (* Psum rcargs *)
-                |> Conv.fconv_rule sum_prod_conv
-                |> Conv.fconv_rule ind_rulify
+                |> Conv.fconv_rule (sum_prod_conv ctxt)
+                |> Conv.fconv_rule (ind_rulify ctxt)
                 |> (fn th => th COMP ipres) (* P rs *)
                 |> fold_rev (Thm.implies_intr o cprop_of) cGas
                 |> fold_rev Thm.forall_intr cGvs
@@ -312,8 +314,9 @@
 
         val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
           |> Goal.init
-          |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
-              THEN CONVERSION ind_rulify 1)
+          |> (Simplifier.rewrite_goals_tac ctxt
+                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+              THEN CONVERSION (ind_rulify ctxt) 1)
           |> Seq.hd
           |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
           |> Goal.finish ctxt
@@ -375,7 +378,7 @@
         indthm
         |> Drule.instantiate' [] [SOME inst]
         |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
-        |> Conv.fconv_rule ind_rulify
+        |> Conv.fconv_rule (ind_rulify ctxt'')
       end
 
     val res = Conjunction.intr_balanced (map_index project branches)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -180,6 +180,7 @@
     val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
     val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
   in 
+    (* FIXME ctxt vs. ctxt' (!?) *)
     rule
     |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
     |> Tactic.rule_by_tactic ctxt
@@ -188,7 +189,7 @@
        THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
     |> (fn thm => thm OF [mono_thm, f_def])
     |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
-         (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}])) 
+         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
     |> singleton (Variable.export ctxt' ctxt)
   end
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/termination.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -305,7 +305,7 @@
   in
     (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
-     THEN rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
+     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
   end
 
 end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -85,7 +85,7 @@
       in
         Conv.fconv_rule 
           ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
-            (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+            (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
       end
 
     fun inst_relcomppI thy ant1 ant2 =
@@ -482,7 +482,7 @@
     val eq_thm = 
       (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
-    Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
+    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end
 
 fun rename_to_tnames ctxt term =
@@ -533,7 +533,8 @@
           fun after_qed' thm_list lthy = 
             let
               val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm 
-                  (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
+                  (fn {context = ctxt, ...} =>
+                    rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
             in
               after_qed internal_rsp_thm lthy
             end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Meson/meson.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -552,9 +552,9 @@
    @{const_name Let}]
 
 fun presimplify ctxt =
-  rewrite_rule (map safe_mk_meta_eq nnf_simps)
+  rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps)
   #> simplify (put_simpset nnf_ss ctxt)
-  #> rewrite_rule @{thms Let_def [abs_def]}
+  #> rewrite_rule ctxt @{thms Let_def [abs_def]}
 
 fun make_nnf ctxt th = case prems_of th of
     [] => th |> presimplify ctxt |> make_nnf1 ctxt
@@ -706,7 +706,7 @@
   Function mkcl converts theorems to clauses.*)
 fun MESON preskolem_tac mkcl cltac ctxt i st =
   SELECT_GOAL
-    (EVERY [Object_Logic.atomize_prems_tac 1,
+    (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
             rtac ccontr 1,
             preskolem_tac,
             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -193,6 +193,8 @@
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
 fun old_skolem_theorem_of_def thy rhs0 =
   let
+    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
+
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
@@ -208,8 +210,8 @@
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.apply cTrueprop
     fun tacf [prem] =
-      rewrite_goals_tac @{thms skolem_def [abs_def]}
-      THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
+      rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
+      THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
                  RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
   in
     Goal.prove_internal [ex_tm] conc tacf
@@ -308,7 +310,7 @@
          |> zero_var_indexes
          |> new_skolem ? forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
-    val th = th |> Conv.fconv_rule Object_Logic.atomize
+    val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
                 |> cong_extensionalize_thm thy
                 |> abs_extensionalize_thm ctxt
                 |> make_nnf ctxt
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -135,8 +135,8 @@
   Isa_Raw of thm
 
 val proxy_defs = map (fst o snd o snd) proxy_table
-val prepare_helper =
-  Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
+fun prepare_helper ctxt =
+  Meson.make_meta_clause #> 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
@@ -160,7 +160,7 @@
 fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
     maps (metis_literals_of_atp type_enc) phis
   | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
-fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
+fun metis_axiom_of_atp ctxt type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
     let
       fun some isa =
         SOME (phi |> metis_literals_of_atp type_enc
@@ -178,7 +178,7 @@
           nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
                |> the)
               (the (Int.fromString j) - 1)
-          |> snd |> prepare_helper
+          |> snd |> prepare_helper ctxt
           |> Isa_Raw |> some
         | _ => raise Fail ("malformed helper identifier " ^ quote ident)
       else case try (unprefix fact_prefix) ident of
@@ -196,7 +196,7 @@
         end
       | NONE => TrueI |> Isa_Raw |> some
     end
-  | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
+  | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
 
 fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
     eliminate_lam_wrappers t
@@ -249,7 +249,7 @@
     (* "rev" is for compatibility with existing proof scripts. *)
     val axioms =
       atp_problem
-      |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
+      |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
     fun ord_info () = atp_problem_term_order_info atp_problem
   in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -249,16 +249,16 @@
    "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
    don't use this trick in general because it makes the proof object uglier than
    necessary. FIXME. *)
-fun negate_head th =
+fun negate_head ctxt th =
   if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
     (th RS @{thm select_FalseI})
-    |> fold (rewrite_rule o single)
+    |> fold (rewrite_rule ctxt o single)
             @{thms not_atomize_select atomize_not_select}
   else
-    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
+    th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
 
 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
-val select_literal = negate_head oo make_last
+fun select_literal ctxt = negate_head ctxt oo make_last
 
 fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
   let
@@ -293,7 +293,7 @@
               i_th2)
            | j2 =>
              (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
-              resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
+              resolve_inc_tyvars thy (select_literal ctxt j1 i_th1) j2 i_th2
               handle TERM (s, _) =>
                      raise METIS_RECONSTRUCT ("resolve_inference", s)))
       end
@@ -448,7 +448,7 @@
                            |> distinct Term.aconv_untyped
         val goal = Logic.list_implies (prems, concl)
         val tac = cut_tac th 1
-                  THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
+                  THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]}
                   THEN ALLGOALS assume_tac
       in
         if length prems = length prems0 then
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -65,7 +65,7 @@
 fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
   let
     val thy = Proof_Context.theory_of ctxt
-    val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
+    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
     val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -219,8 +219,8 @@
           |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
         val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
         val case_th =
-          rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
-        val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
+          rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
+        val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
         val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
         val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
           OF (replicate nargs @{thm refl})
@@ -236,7 +236,7 @@
       (PEEK nprems_of
         (fn n =>
           ALLGOALS (fn i =>
-            rewrite_goal_tac [@{thm split_paired_all}] i
+            rewrite_goal_tac ctxt [@{thm split_paired_all}] i
             THEN (SUBPROOF (instantiate i n) ctxt i))))
   in
     Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -1017,8 +1017,9 @@
 
 fun peephole_optimisation thy intro =
   let
+    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val process =
-      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
+      rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
     fun process_False intro_t =
       if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
     fun process_True intro_t =
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -203,7 +203,7 @@
     SOME specss => (specss, thy)
   | NONE =>*)
     let
-      val ctxt = Proof_Context.init_global thy
+      val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
       val intros =
         if forall is_pred_equation specs then 
           map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
@@ -213,7 +213,7 @@
           error ("unexpected specification for constant " ^ quote constname ^ ":\n"
             ^ commas (map (quote o Display.string_of_thm_global thy) specs))
       val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
-      val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
+      val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
       val _ = print_specs options thy "normalized intros" intros
       (*val intros = maps (split_cases thy) intros*)
       val (intros', (local_defs, thy')) = flatten_intros constname intros thy
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -79,11 +79,11 @@
          @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
          @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
     | Free _ =>
-      Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
+      Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
         let
           val prems' = maps dest_conjunct_prem (take nargs prems)
         in
-          rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+          rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
         end) ctxt 1
     | Abs _ => raise Fail "prove_param: No valid parameter term"
   in
@@ -118,7 +118,7 @@
       end
   | (Free _, _) =>
     print_tac options "proving parameter call.."
-    THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
+    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
         let
           val param_prem = nth prems premposition
           val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
@@ -126,7 +126,7 @@
           fun param_rewrite prem =
             param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
           val SOME rew_eq = find_first param_rewrite prems'
-          val param_prem' = rewrite_rule
+          val param_prem' = rewrite_rule ctxt'
             (map (fn th => th RS @{thm eq_reflection})
               [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
             param_prem
@@ -168,7 +168,7 @@
                 let
                   val prems' = maps dest_conjunct_prem (take nargs prems)
                 in
-                  rewrite_goal_tac
+                  rewrite_goal_tac ctxt
                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
                 end
              THEN REPEAT_DETERM (rtac @{thm refl} 1))
@@ -205,12 +205,12 @@
       THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
       THEN print_tac options "before single intro rule"
       THEN Subgoal.FOCUS_PREMS
-             (fn {context, params, prems, asms, concl, schematics} =>
-              let
-                val prems' = maps dest_conjunct_prem (take nargs prems)
-              in
-                rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
-              end) ctxt 1
+         (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+          let
+            val prems' = maps dest_conjunct_prem (take nargs prems)
+          in
+            rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+          end) ctxt 1
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, deriv) :: ps) =
       let
@@ -293,7 +293,7 @@
     val nargs = length (binder_types T)
     val pred_case_rule = the_elim_of ctxt pred
   in
-    REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))
+    REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
     THEN print_tac options "before applying elim rule"
     THEN etac (predfun_elim_of ctxt pred mode) 1
     THEN etac pred_case_rule 1
@@ -370,7 +370,7 @@
           val ho_args = ho_args_of mode args
         in
           etac @{thm bindE} 1
-          THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
+          THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
           THEN print_tac options "prove_expr2-before"
           THEN etac (predfun_elim_of ctxt name mode) 1
           THEN print_tac options "prove_expr2"
@@ -483,11 +483,11 @@
       THEN (prove_clause2 options ctxt pred mode clause i)
   in
     (DETERM (TRY (rtac @{thm unit.induct} 1)))
-     THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
+     THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
      THEN (rtac (predfun_intro_of ctxt pred mode) 1)
      THEN (REPEAT_DETERM (rtac @{thm refl} 2))
-     THEN (if null moded_clauses then
-         etac @{thm botE} 1
+     THEN (
+       if null moded_clauses then etac @{thm botE} 1
        else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
   end;
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -865,19 +865,19 @@
     val aprems = Arith_Data.get_arith_facts ctxt
   in
     Method.insert_tac aprems
-    THEN_ALL_NEW Object_Logic.full_atomize_tac
+    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
     THEN_ALL_NEW simp_tac simpset_ctxt
     THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
-    THEN_ALL_NEW Object_Logic.full_atomize_tac
+    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
-    THEN_ALL_NEW Object_Logic.full_atomize_tac
+    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     THEN_ALL_NEW div_mod_tac ctxt
     THEN_ALL_NEW splits_tac ctxt
     THEN_ALL_NEW simp_tac simpset_ctxt
     THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
     THEN_ALL_NEW nat_to_int_tac ctxt
-    THEN_ALL_NEW (core_tac ctxt)
+    THEN_ALL_NEW core_tac ctxt
     THEN_ALL_NEW finish_tac elim
   end 1);
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -107,7 +107,7 @@
     fun tac ctxt =
       ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
-      THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
+      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
     val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
   in (simp, lthy') end;
 
@@ -166,7 +166,7 @@
     fun prove_simps proto_simps lthy =
       let
         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
-        val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
+        val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
       in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
     val b = Binding.conceal (Binding.qualify true prfx
       (Binding.qualify true name (Binding.name "simps")));
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -129,7 +129,7 @@
     val eq_thm = 
       (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
-    Object_Logic.rulify (eq_thm RS Drule.equal_elim_rule2)
+    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end
 
 
@@ -187,7 +187,7 @@
           case thm_list of
             [] => the maybe_proven_rsp_thm
           | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm 
-            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
+            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
       in
         snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
       end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -40,10 +40,10 @@
 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
-fun atomize_thm thm =
+fun atomize_thm ctxt thm =
   let
     val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
-    val thm'' = Object_Logic.atomize (cprop_of thm')
+    val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
   in
     @{thm equal_elim_rule1} OF [thm'', thm']
   end
@@ -480,7 +480,7 @@
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
-        val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
+        val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
         val (insp, inst) =
           if ty_c = ty_d
           then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
@@ -635,7 +635,7 @@
     val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
   in
     full_simp_tac simpset
-    THEN' Object_Logic.full_atomize_tac
+    THEN' Object_Logic.full_atomize_tac ctxt
     THEN' gen_frees_tac ctxt
     THEN' SUBGOAL (fn (goal, i) =>
       let
@@ -652,7 +652,7 @@
     val mk_tac_raw =
       descend_procedure_tac ctxt simps
       THEN' RANGE
-        [Object_Logic.rulify_tac THEN' (K all_tac),
+        [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
          regularize_tac ctxt,
          all_injection_tac ctxt,
          clean_tac ctxt]
@@ -685,7 +685,7 @@
     val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
   in
     full_simp_tac simpset
-    THEN' Object_Logic.full_atomize_tac
+    THEN' Object_Logic.full_atomize_tac ctxt
     THEN' gen_frees_tac ctxt
     THEN' SUBGOAL (fn (goal, i) =>
       let
@@ -702,7 +702,7 @@
     val mk_tac_raw =
       partiality_descend_procedure_tac ctxt simps
       THEN' RANGE
-        [Object_Logic.rulify_tac THEN' (K all_tac),
+        [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
          all_injection_tac ctxt,
          clean_tac ctxt]
   in
@@ -720,7 +720,7 @@
     val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
   in
     full_simp_tac simpset
-    THEN' Object_Logic.full_atomize_tac
+    THEN' Object_Logic.full_atomize_tac ctxt
     THEN' gen_frees_tac ctxt
     THEN' SUBGOAL (fn (goal, i) =>
       let
@@ -730,7 +730,7 @@
           rthm |> full_simplify simpset
                |> Drule.eta_contraction_rule
                |> Thm.forall_intr_frees
-               |> atomize_thm
+               |> atomize_thm ctxt
 
         val rule = procedure_inst ctxt (prop_of rthm') goal
       in
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -193,7 +193,7 @@
     val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
     val quotient_thm =
       (quot_thm RS @{thm quot_type.Quotient})
-      |> fold_rule [abs_def, rep_def]
+      |> fold_rule lthy3 [abs_def, rep_def]
 
     (* name equivalence theorem *)
     val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -68,7 +68,7 @@
 fun prove_inj_prop ctxt def lhs =
   let
     val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
-    val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
+    val rule = disjE OF [Object_Logic.rulify ctxt (Thm.assume lhs)]
   in
     Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
     |> apply (rtac @{thm injI})
@@ -94,7 +94,7 @@
 
 fun prove_lhs ctxt rhs =
   let
-    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
+    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
     val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
   in
     Z3_Proof_Tools.by_tac (
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -38,16 +38,19 @@
     val merge = Net.merge eq
   )
 
-  val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
+  fun prep context =
+    `Thm.prop_of o rewrite_rule (Context.proof_of context) [Z3_Proof_Literals.rewrite_true]
 
-  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
-  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
+  fun ins thm context =
+    context |> Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
+  fun rem thm context =
+    context |> Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
 
-  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
-  val del = Thm.declaration_attribute (Z3_Rules.map o del)
+  val add = Thm.declaration_attribute ins
+  val del = Thm.declaration_attribute rem
 in
 
-val add_z3_rule = Z3_Rules.map o ins
+val add_z3_rule = ins
 
 fun by_schematic_rule ctxt ct =
   the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/TFL/post.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -68,10 +68,11 @@
   |   _ => r RS P_imp_P_eq_True
 
 (*Is this the best way to invoke the simplifier??*)
-fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
+fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
 
 fun join_assums th =
   let val thy = Thm.theory_of_thm th
+      val ctxt = Proof_Context.init_global thy
       val tych = cterm_of thy
       val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
       val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
@@ -80,7 +81,7 @@
   in
     Rules.GEN_ALL
       (Rules.DISCH_ALL
-         (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
+         (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
   end
   val gen_all = USyntax.gen_all
 in
@@ -139,7 +140,7 @@
    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, (def, pats))
+           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 "congs =" congs
@@ -149,9 +150,9 @@
                {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)
+       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 (induction RS spec')),
+         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
@@ -170,7 +171,7 @@
     | solve_eq _ (th, [a], i) = [(a, i)]
     | solve_eq ctxt (th, splitths, i) =
       (writeln "Proving unsplit equation...";
-      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
+      [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
           (CaseSplit.splitto ctxt splitths th), i)])
       handle ERROR s => 
              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/TFL/rules.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -42,14 +42,14 @@
   val DISJ_CASESL: thm -> thm list -> thm
 
   val list_beta_conv: cterm -> cterm list -> thm
-  val SUBS: thm list -> thm -> thm
+  val SUBS: Proof.context -> thm list -> thm -> thm
   val simpl_conv: Proof.context -> thm list -> cterm -> thm
 
   val rbeta: thm -> thm
   val tracing: bool Unsynchronized.ref
   val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
                              -> thm -> thm * term list
-  val RIGHT_ASSOC: thm -> thm
+  val RIGHT_ASSOC: Proof.context -> thm -> thm
 
   val prove: bool -> cterm * tactic -> thm
 end;
@@ -417,8 +417,8 @@
  *        Rewriting
  *---------------------------------------------------------------------------*)
 
-fun SUBS thl =
-  rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
+fun SUBS ctxt thl =
+  rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
 
 val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
 
@@ -426,7 +426,7 @@
  rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
 
 
-val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
+fun RIGHT_ASSOC ctxt = rewrite_rule ctxt [Thms.disj_assoc];
 
 
 
@@ -602,24 +602,24 @@
  *  the wrong word to use).
  *---------------------------------------------------------------------------*)
 
-fun VSTRUCT_ELIM tych a vstr th =
+fun VSTRUCT_ELIM ctxt tych a vstr th =
   let val L = USyntax.free_vars_lr vstr
       val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
-      val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
+      val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
       val thm2 = forall_intr_list (map tych L) thm1
       val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   in refl RS
-     rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
+     rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
   end;
 
-fun PGEN tych a vstr th =
+fun PGEN ctxt tych a vstr th =
   let val a1 = tych a
       val vstr1 = tych vstr
   in
   Thm.forall_intr a1
      (if (is_Free vstr)
       then cterm_instantiate [(vstr1,a1)] th
-      else VSTRUCT_ELIM tych a vstr th)
+      else VSTRUCT_ELIM ctxt tych a vstr th)
   end;
 
 
@@ -701,7 +701,7 @@
                   val impth = implies_intr_list ants1 QeeqQ3
                   val impth1 = impth RS meta_eq_to_obj_eq
                   (* Need to abstract *)
-                  val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
+                  val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
               in ant_th COMP thm
               end
              fun q_eliminate (thm,imp,thy) =
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/TFL/tfl.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -12,7 +12,7 @@
   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 * (thm * pattern list) ->
+  val post_definition: thm list -> theory -> Proof.context -> thm * pattern list ->
    {rules: thm,
     rows: int list,
     TCs: term list list,
@@ -415,7 +415,7 @@
 
 fun givens pats = map pat_of (filter given pats);
 
-fun post_definition meta_tflCongs (theory, (def, pats)) =
+fun post_definition meta_tflCongs theory ctxt (def, pats) =
  let val tych = Thry.typecheck theory
      val f = #lhs(USyntax.dest_eq(concl def))
      val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
@@ -440,7 +440,7 @@
      val extract = Rules.CONTEXT_REWRITE_RULE
                      (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
-     val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
+     val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
      val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
      val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
  in
@@ -460,7 +460,8 @@
  *---------------------------------------------------------------------------*)
 
 fun wfrec_eqns thy fid tflCongs eqns =
- let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
+ let val ctxt = Proof_Context.init_global thy
+     val {lhs,rhs} = USyntax.dest_eq (hd eqns)
      val (f,args) = USyntax.strip_comb lhs
      val (fname,fty) = dest_atom f
      val (SV,a) = front_last args    (* SV = schematic variables *)
@@ -493,7 +494,7 @@
      val R1 = USyntax.rand WFR
      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 case_rewrites) corollaries
+     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
  in {proto_def = proto_def,
@@ -625,6 +626,7 @@
 
 fun mk_case ty_info usednames thy =
  let
+ val ctxt = Proof_Context.init_global thy
  val divide = ipartition (gvvariant usednames)
  val tych = Thry.typecheck thy
  fun tych_binding(x,y) = (tych x, tych y)
@@ -657,7 +659,7 @@
                                    (new_formals, disjuncts)
             val constraints = map #1 existentials
             val vexl = map #2 existentials
-            fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
+            fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
             val news = map (fn (nf,rows,c) => {path = nf@rstp,
                                                rows = map (expnd c) rows})
                            (Utils.zip3 new_formals groups constraints)
@@ -675,7 +677,8 @@
 
 
 fun complete_cases thy =
- let val tych = Thry.typecheck thy
+ let val ctxt = Proof_Context.init_global thy
+     val tych = Thry.typecheck thy
      val ty_info = Thry.induct_info thy
  in fn pats =>
  let val names = List.foldr Misc_Legacy.add_term_names [] pats
@@ -691,7 +694,7 @@
      val rows = map (fn x => ([x], (th0,[]))) pats
  in
  Rules.GEN (tych a)
-       (Rules.RIGHT_ASSOC
+       (Rules.RIGHT_ASSOC ctxt
           (Rules.CHOOSE(tych v, ex_th0)
                 (mk_case ty_info (vname::aname::names)
                  thy {path=[v], rows=rows})))
@@ -826,7 +829,8 @@
  * the antecedent of Rinduct.
  *---------------------------------------------------------------------------*)
 fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
-let val tych = Thry.typecheck thy
+let val ctxt = Proof_Context.init_global thy
+    val tych = Thry.typecheck thy
     val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
@@ -848,7 +852,7 @@
           domain)
     val vtyped = tych v
     val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
-    val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
+    val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
                           (substs, proved_cases)
     val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
     val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/choice_specification.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -113,6 +113,8 @@
 
 fun process_spec axiomatic cos alt_props thy =
     let
+        val ctxt = Proof_Context.init_global thy
+
         fun zip3 [] [] [] = []
           | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
           | zip3 _ _ _ = error "Choice_Specification.process_spec internal error"
@@ -122,7 +124,7 @@
           | myfoldr f [] = error "Choice_Specification.process_spec internal error"
 
         val rew_imps = alt_props |>
-          map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
+          map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
         val props' = rew_imps |>
           map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/coinduction.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -53,9 +53,9 @@
     val cases = Rule_Cases.get raw_thm |> fst
   in
     NO_CASES (HEADGOAL (
-      Object_Logic.rulify_tac THEN'
+      Object_Logic.rulify_tac ctxt THEN'
       Method.insert_tac prems THEN'
-      Object_Logic.atomize_prems_tac THEN'
+      Object_Logic.atomize_prems_tac ctxt THEN'
       DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
         let
           val vars = raw_vars @ map (term_of o snd) params;
@@ -110,7 +110,7 @@
                         unfold_thms_tac ctxt eqs
                       end)) ctxt)))])
         end) ctxt) THEN'
-      K (prune_params_tac))) st
+      K (prune_params_tac ctxt))) st
     |> Seq.maps (fn (_, st) =>
       CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
   end;
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/groebner.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -928,7 +928,7 @@
     delsimps del_thms addsimps add_thms);
 
 fun ring_tac add_ths del_ths ctxt =
-  Object_Logic.full_atomize_tac
+  Object_Logic.full_atomize_tac ctxt
   THEN' presimplify ctxt add_ths del_ths
   THEN' CSUBGOAL (fn (p, i) =>
     rtac (let val form = Object_Logic.dest_judgment p
@@ -970,7 +970,7 @@
    end
   in
      clarify_tac (put_claset claset ctxt) i
-     THEN Object_Logic.full_atomize_tac i
+     THEN Object_Logic.full_atomize_tac ctxt i
      THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
      THEN clarify_tac (put_claset claset ctxt) i
      THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/inductive.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -396,7 +396,7 @@
 
     val intrs = map_index (fn (i, intr) =>
       Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
-       [rewrite_goals_tac rec_preds_defs,
+       [rewrite_goals_tac ctxt rec_preds_defs,
         rtac (unfold RS iffD2) 1,
         EVERY1 (select_disj (length intr_ts) (i + 1)),
         (*Not ares_tac, since refl must be tried before any equality assumptions;
@@ -440,14 +440,15 @@
            map mk_elim_prem (map #1 c_intrs)
       in
         (Goal.prove_sorry ctxt'' [] prems P
-          (fn {prems, ...} => EVERY
+          (fn {context = ctxt4, prems} => EVERY
             [cut_tac (hd prems) 1,
-             rewrite_goals_tac rec_preds_defs,
+             rewrite_goals_tac ctxt4 rec_preds_defs,
              dtac (unfold RS iffD1) 1,
              REPEAT (FIRSTGOAL (eresolve_tac rules1)),
              REPEAT (FIRSTGOAL (eresolve_tac rules2)),
              EVERY (map (fn prem =>
-               DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
+               DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
+                (tl prems))])
           |> singleton (Proof_Context.export ctxt'' ctxt'''),
          map #2 c_intrs, length Ts)
       end
@@ -503,12 +504,12 @@
           (if null ts andalso null us then rtac intr 1
            else
             EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
-            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
+            Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
               let
                 val (eqs, prems') = chop (length us) prems;
                 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
               in
-                rewrite_goal_tac rew_thms 1 THEN
+                rewrite_goal_tac ctxt'' rew_thms 1 THEN
                 rtac intr 1 THEN
                 EVERY (map (fn p => rtac p 1) prems')
               end) ctxt' 1);
@@ -545,7 +546,7 @@
 
 in
 
-fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
+fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt;
 
 fun mk_cases ctxt prop =
   let
@@ -598,7 +599,7 @@
           val props = Syntax.read_props ctxt' raw_props;
           val ctxt'' = fold Variable.declare_term props ctxt';
           val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
-        in Method.erule 0 rules end))
+        in Method.erule ctxt 0 rules end))
     "dynamic case analysis on predicates";
 
 
@@ -724,30 +725,30 @@
     val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
 
     val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
-      (fn {prems, ...} => EVERY
-        [rewrite_goals_tac [inductive_conj_def],
+      (fn {context = ctxt3, prems} => EVERY
+        [rewrite_goals_tac ctxt3 [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
          REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
-         rewrite_goals_tac simp_thms2,
+         rewrite_goals_tac ctxt3 simp_thms2,
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
-         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
+         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
-         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
+         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
              (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
            conjI, refl] 1)) prems)]);
 
     val lemma = Goal.prove_sorry ctxt'' [] []
-      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
-        [rewrite_goals_tac rec_preds_defs,
+      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
+        [rewrite_goals_tac ctxt3 rec_preds_defs,
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
             REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
             atac 1,
-            rewrite_goals_tac simp_thms1,
+            rewrite_goals_tac ctxt3 simp_thms1,
             atac 1])]);
 
   in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
@@ -961,9 +962,9 @@
       (if no_ind then Drule.asm_rl
        else if coind then
          singleton (Proof_Context.export lthy2 lthy1)
-           (rotate_prems ~1 (Object_Logic.rulify
-             (fold_rule rec_preds_defs
-               (rewrite_rule simp_thms3
+           (rotate_prems ~1 (Object_Logic.rulify lthy2
+             (fold_rule lthy2 rec_preds_defs
+               (rewrite_rule lthy2 simp_thms3
                 (mono RS (fp_def RS @{thm def_coinduct}))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -393,11 +393,11 @@
         val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
         val thm = Goal.prove_global thy []
           (map attach_typeS prems) (attach_typeS concl)
-          (fn {prems, ...} => EVERY
+          (fn {context = ctxt, prems} => EVERY
           [rtac (#raw_induct ind_info) 1,
-           rewrite_goals_tac rews,
+           rewrite_goals_tac ctxt rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
-             [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
+             [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
           (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
@@ -459,8 +459,8 @@
             [cut_tac (hd prems) 1,
              etac elimR 1,
              ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
-             rewrite_goals_tac rews,
-             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
+             rewrite_goals_tac ctxt rews,
+             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/lin_arith.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -871,8 +871,9 @@
 
 in
 
-fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
-  Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+fun gen_tac ex ctxt =
+  FIRST' [simple_tac ctxt,
+    Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
 
 val tac = gen_tac true;
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/nat_arith.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -6,10 +6,10 @@
 
 signature NAT_ARITH =
 sig
-  val cancel_diff_conv: conv
-  val cancel_eq_conv: conv
-  val cancel_le_conv: conv
-  val cancel_less_conv: conv
+  val cancel_diff_conv: Proof.context -> conv
+  val cancel_eq_conv: Proof.context -> conv
+  val cancel_le_conv: Proof.context -> conv
+  val cancel_less_conv: Proof.context -> conv
 end;
 
 structure Nat_Arith: NAT_ARITH =
@@ -26,9 +26,9 @@
 
 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
 
-fun move_to_front path = Conv.every_conv
+fun move_to_front ctxt path = Conv.every_conv
     [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
-     Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
+     Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
 
 fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
       add_atoms (add1::path) x #> add_atoms (add2::path) y
@@ -54,12 +54,12 @@
     find (sort ord' xs) (sort ord' ys)
   end
 
-fun cancel_conv rule ct =
+fun cancel_conv rule ctxt ct =
   let
     val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
     val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
-    val lconv = move_to_front lpath
-    val rconv = move_to_front rpath
+    val lconv = move_to_front ctxt lpath
+    val rconv = move_to_front ctxt rpath
     val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
     val conv = conv1 then_conv Conv.rewr_conv rule
   in conv ct end
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/record.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -1616,9 +1616,9 @@
 
     val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_meta_prop
-        (fn _ =>
+        (fn {context = ctxt, ...} =>
           EVERY1
-           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
+           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
             etac @{thm meta_allE}, atac,
             rtac (@{thm prop_subst} OF [surject]),
             REPEAT o etac @{thm meta_allE}, atac]));
@@ -1742,12 +1742,13 @@
         HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
            Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
-      fun tac eq_def =
+      fun tac ctxt eq_def =
         Class.intro_classes_tac []
-        THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
+        THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
         THEN ALLGOALS (rtac @{thm refl});
       fun mk_eq thy eq_def =
-        rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
+        rewrite_rule (Proof_Context.init_global thy)
+          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
       fun mk_eq_refl thy =
         @{thm equal_refl}
         |> Thm.instantiate
@@ -1765,8 +1766,7 @@
       |-> (fn eq => Specification.definition
             (NONE, (Attrib.empty_binding, eq)))
       |-> (fn (_, (_, eq_def)) =>
-         Class.prove_instantiation_exit_result Morphism.thm
-            (fn _ => fn eq_def => tac eq_def) eq_def)
+         Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
       |-> (fn eq_def => fn thy =>
             thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
       |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
@@ -2139,18 +2139,18 @@
 
     val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_meta_prop
-        (fn _ =>
+        (fn {context = ctxt', ...} =>
           EVERY1
-           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
+           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
             etac @{thm meta_allE}, atac,
             rtac (@{thm prop_subst} OF [surjective]),
             REPEAT o etac @{thm meta_allE}, atac]));
 
     val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_object_prop
-        (fn _ =>
+        (fn {context = ctxt, ...} =>
           rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
-          rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
+          rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
           rtac split_meta 1));
 
     val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/sat_funcs.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -427,9 +427,9 @@
 (*      subgoal                                                              *)
 (* ------------------------------------------------------------------------- *)
 
-val pre_cnf_tac =
+fun pre_cnf_tac ctxt =
   rtac ccontr THEN'
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   CONVERSION Drule.beta_eta_conversion;
 
 (* ------------------------------------------------------------------------- *)
@@ -460,7 +460,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun sat_tac ctxt i =
-  pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
+  pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
@@ -469,6 +469,6 @@
 (* ------------------------------------------------------------------------- *)
 
 fun satx_tac ctxt i =
-  pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
+  pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
 
 end;
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/simpdata.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -71,10 +71,10 @@
         Goal.prove_global (Thm.theory_of_thm st) []
           [mk_simp_implies @{prop "(x::'a) == y"}]
           (mk_simp_implies @{prop "(x::'a) = y"})
-          (fn {prems, ...} => EVERY
-           [rewrite_goals_tac @{thms simp_implies_def},
+          (fn {context = ctxt, prems} => EVERY
+           [rewrite_goals_tac ctxt @{thms simp_implies_def},
             REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
-              map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
+              map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
       end
   end;
 
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/transfer.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -193,7 +193,7 @@
     by (unfold is_equality_def, rule, drule meta_spec,
       erule meta_mp, rule refl, simp)}
 
-fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
+fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
   let
     val thy = Thm.theory_of_thm thm
     val prop = Thm.prop_of thm
@@ -212,7 +212,7 @@
     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
     val cprop = Thm.cterm_of thy prop2
-    val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
+    val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -234,11 +234,11 @@
       Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
       handle CTERM _ => thm
   in
-    gen_abstract_equalities dest contracted_eq_thm
+    gen_abstract_equalities ctxt dest contracted_eq_thm
   end
 
-fun abstract_equalities_relator_eq rel_eq_thm =
-  gen_abstract_equalities (fn x => (x, I))
+fun abstract_equalities_relator_eq ctxt rel_eq_thm =
+  gen_abstract_equalities ctxt (fn x => (x, I))
     (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
 
 fun abstract_equalities_domain ctxt thm =
@@ -256,7 +256,7 @@
     val contracted_eq_thm = 
       Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
   in
-    gen_abstract_equalities dest contracted_eq_thm
+    gen_abstract_equalities ctxt dest contracted_eq_thm
   end 
 
 
@@ -288,7 +288,7 @@
           | t => t)
   end
 
-fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
+fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
   let
     val thy = Thm.theory_of_thm thm
     val prop = Thm.prop_of thm
@@ -305,14 +305,14 @@
     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
     val prop2 = Logic.list_rename_params (rev names) prop1
     val cprop = Thm.cterm_of thy prop2
-    val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
+    val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   end
     handle TERM _ => thm
 
-fun abstract_domains_transfer thm =
+fun abstract_domains_transfer ctxt thm =
   let
     fun dest prop =
       let
@@ -324,7 +324,7 @@
           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
       end
   in
-    gen_abstract_domains dest thm
+    gen_abstract_domains ctxt dest thm
   end
 
 fun detect_transfer_rules thm =
@@ -587,11 +587,11 @@
         handle TERM (_, ts) => raise TERM (err_msg, ts)
   in
     EVERY
-      [rewrite_goal_tac pre_simps i THEN
+      [rewrite_goal_tac ctxt pre_simps i THEN
        SUBGOAL main_tac i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
-       rewrite_goal_tac post_simps i,
-       Goal.norm_hhf_tac i]
+       rewrite_goal_tac ctxt post_simps i,
+       Goal.norm_hhf_tac ctxt i]
   end
 
 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
@@ -626,7 +626,7 @@
                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     val thm2 = thm1
       |> Thm.certify_instantiate (instT, [])
-      |> Raw_Simplifier.rewrite_rule pre_simps
+      |> 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)
     val rule = transfer_rule_of_lhs ctxt' t
@@ -641,7 +641,7 @@
     val tnames = map (fst o dest_TFree o snd) instT
   in
     thm3
-      |> Raw_Simplifier.rewrite_rule post_simps
+      |> Raw_Simplifier.rewrite_rule ctxt' post_simps
       |> Raw_Simplifier.norm_hhf
       |> Drule.generalize (tnames, [])
       |> Drule.zero_var_indexes
@@ -662,7 +662,7 @@
                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     val thm2 = thm1
       |> Thm.certify_instantiate (instT, [])
-      |> Raw_Simplifier.rewrite_rule pre_simps
+      |> 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)
     val rule = transfer_rule_of_term ctxt' true t
@@ -677,7 +677,7 @@
     val tnames = map (fst o dest_TFree o snd) instT
   in
     thm3
-      |> Raw_Simplifier.rewrite_rule post_simps
+      |> Raw_Simplifier.rewrite_rule ctxt' post_simps
       |> Raw_Simplifier.norm_hhf
       |> Drule.generalize (tnames, [])
       |> Drule.zero_var_indexes
@@ -700,8 +700,8 @@
 
 (* Attribute for transfer rules *)
 
-fun prep_rule ctxt thm = 
-  (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm
+fun prep_rule ctxt = 
+  abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
 
 val transfer_add =
   Thm.declaration_attribute (fn thm => fn ctxt => 
@@ -742,10 +742,14 @@
 val relator_eq_setup =
   let
     val name = @{binding relator_eq}
-    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
-      #> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
-    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
-      #> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
+    fun add_thm thm context = context
+      |> Data.map (map_relator_eq (Item_Net.update thm))
+      |> Data.map (map_relator_eq_raw
+          (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
+    fun del_thm thm context = context
+      |> Data.map (map_relator_eq (Item_Net.remove thm))
+      |> Data.map (map_relator_eq_raw
+          (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
     val add = Thm.declaration_attribute add_thm
     val del = Thm.declaration_attribute del_thm
     val text = "declaration of relator equality rule (used by transfer method)"
diff -r 7068557b7c63 -r 283fc522d24e src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Word/Word.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -14,7 +14,7 @@
   Word_Miscellaneous
 begin
 
-text {* see @{text "Examples/WordExamples.thy"} for examples *}
+text {* See @{file "Examples/WordExamples.thy"} for examples. *}
 
 subsection {* Type definition *}
 
@@ -1463,7 +1463,7 @@
         (put_simpset HOL_ss ctxt
           |> fold Splitter.add_split @{thms uint_splits}
           |> fold Simplifier.add_cong @{thms power_False_cong})),
-      rewrite_goals_tac @{thms word_size}, 
+      rewrite_goals_tac ctxt @{thms word_size}, 
       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
                          REPEAT (etac conjE n) THEN
                          REPEAT (dtac @{thm word_of_int_inverse} n 
@@ -1964,7 +1964,7 @@
         (put_simpset HOL_ss ctxt
           |> fold Splitter.add_split @{thms unat_splits}
           |> fold Simplifier.add_cong @{thms power_False_cong})),
-      rewrite_goals_tac @{thms word_size}, 
+      rewrite_goals_tac ctxt @{thms word_size}, 
       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
                          REPEAT (etac conjE n) THEN
                          REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
diff -r 7068557b7c63 -r 283fc522d24e src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/blast.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -1265,7 +1265,7 @@
 
 fun depth_tac ctxt lim i st =
   SELECT_GOAL
-    (Object_Logic.atomize_prems_tac 1 THEN
+    (Object_Logic.atomize_prems_tac ctxt 1 THEN
       raw_blast (Timing.start ()) ctxt lim) i st;
 
 fun blast_tac ctxt i st =
@@ -1274,7 +1274,7 @@
     val lim = Config.get ctxt depth_limit;
   in
     SELECT_GOAL
-     (Object_Logic.atomize_prems_tac 1 THEN
+     (Object_Logic.atomize_prems_tac ctxt 1 THEN
       DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
   end;
 
diff -r 7068557b7c63 -r 283fc522d24e src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/clasimp.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -150,7 +150,7 @@
     TRY (Classical.safe_tac ctxt) THEN
     REPEAT_DETERM (FIRSTGOAL main_tac) THEN
     TRY (Classical.safe_tac (addSss ctxt)) THEN
-    prune_params_tac
+    prune_params_tac ctxt
   end;
 
 fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
diff -r 7068557b7c63 -r 283fc522d24e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/classical.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -166,7 +166,13 @@
   else rule;
 
 (*flatten nested meta connectives in prems*)
-val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
+fun flat_rule opt_context th =
+  let
+    val ctxt =
+      (case opt_context of
+        NONE => Proof_Context.init_global (Thm.theory_of_thm th)
+      | SOME context => Context.proof_of context);
+  in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
 
 
 (*** Useful tactics for classical reasoning ***)
@@ -325,7 +331,7 @@
   if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   else
     let
-      val th' = flat_rule th;
+      val th' = flat_rule context th;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition Thm.no_prems [th'];
       val nI = Item_Net.length safeIs + 1;
@@ -354,7 +360,7 @@
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
-      val th' = classical_rule (flat_rule th);
+      val th' = classical_rule (flat_rule context th);
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition (fn rl => nprems_of rl=1) [th'];
       val nI = Item_Net.length safeIs;
@@ -386,7 +392,7 @@
   if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   else
     let
-      val th' = flat_rule th;
+      val th' = flat_rule context th;
       val nI = Item_Net.length hazIs + 1;
       val nE = Item_Net.length hazEs;
       val _ = warn_claset context th cs;
@@ -415,7 +421,7 @@
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
-      val th' = classical_rule (flat_rule th);
+      val th' = classical_rule (flat_rule context th);
       val nI = Item_Net.length hazIs;
       val nE = Item_Net.length hazEs + 1;
       val _ = warn_claset context th cs;
@@ -443,12 +449,12 @@
         to insert.
 ***)
 
-fun delSI th
+fun delSI context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeIs th then
     let
-      val th' = flat_rule th;
+      val th' = flat_rule context th;
       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
     in
       CS
@@ -466,12 +472,12 @@
     end
   else cs;
 
-fun delSE th
+fun delSE context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeEs th then
     let
-      val th' = classical_rule (flat_rule th);
+      val th' = classical_rule (flat_rule context th);
       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
     in
       CS
@@ -493,7 +499,7 @@
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazIs th then
-    let val th' = flat_rule th in
+    let val th' = flat_rule context th in
       CS
        {haz_netpair = delete ([th'], []) haz_netpair,
         dup_netpair = delete ([dup_intr th'], []) dup_netpair,
@@ -511,11 +517,11 @@
   handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
     error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
 
-fun delE th
+fun delE context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazEs th then
-    let val th' = classical_rule (flat_rule th) in
+    let val th' = classical_rule (flat_rule context th) in
       CS
        {haz_netpair = delete ([], [th']) haz_netpair,
         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
@@ -537,7 +543,11 @@
     if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
       Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
       Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
-    then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
+    then
+      delSI context th
+        (delSE context th
+          (delI context th
+            (delE context th (delSE context th' (delE context th' cs)))))
     else (warn_thm context "Undeclared classical rule\n" th; cs)
   end;
 
@@ -774,24 +784,24 @@
 
 (*Dumb but fast*)
 fun fast_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
+  Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 (*Slower but smarter than fast_tac*)
 fun best_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
 
 (*even a bit smarter than best_tac*)
 fun first_best_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
 
 fun slow_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
 
 fun slow_best_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
 
 
@@ -800,13 +810,13 @@
 val weight_ASTAR = 5;
 
 fun astar_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
       (step_tac ctxt 1));
 
 fun slow_astar_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
       (slow_step_tac ctxt 1));
@@ -901,12 +911,12 @@
   in
     fn st => Seq.maps (fn rule => rtac rule i st) ruleq
   end)
-  THEN_ALL_NEW Goal.norm_hhf_tac;
+  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
 
 in
 
 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
-  | rule_tac _ rules facts = Method.rule_tac rules facts;
+  | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
 
 fun default_tac ctxt rules facts =
   HEADGOAL (rule_tac ctxt rules facts) ORELSE
@@ -941,7 +951,7 @@
     (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
     "apply some intro/elim rule (potentially classical)" #>
   Method.setup @{binding contradiction}
-    (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
+    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
     "proof by contradiction" #>
   Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
     "repeatedly apply safe steps" #>
diff -r 7068557b7c63 -r 283fc522d24e src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/splitter.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -100,7 +100,7 @@
 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
-  (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
+  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
 
 val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
 
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/class.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -656,7 +656,7 @@
   | default_intro_tac _ _ = no_tac;
 
 fun default_tac rules ctxt facts =
-  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
+  HEADGOAL (Method.some_rule_tac ctxt rules facts) ORELSE
     default_intro_tac ctxt facts;
 
 val _ = Theory.setup
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/class_declaration.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -58,7 +58,7 @@
             (_, NONE) => all_tac
           | (_, SOME intro) => ALLGOALS (rtac intro));
         val tac = loc_intro_tac
-          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
+          THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
       in Element.prove_witness empty_ctxt prop tac end) some_prop;
     val some_axiom = Option.map Element.conclude_witness some_witn;
 
@@ -77,8 +77,10 @@
             SOME eq_morph => const_morph $> eq_morph
           | NONE => const_morph);
         val thm'' = Morphism.thm const_eq_morph thm';
-        val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
-      in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+      in
+        Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
+          (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
+      end;
     val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
 
     (* of_class *)
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/code.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -1130,9 +1130,12 @@
     fun mk_prem z = Free (z, T_cong);
     fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
     val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
-    fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
-      THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
-  in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
+  in
+    Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl
+      (fn {context = ctxt', prems} =>
+        Simplifier.rewrite_goals_tac ctxt' prems
+        THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm]))
+  end;
 
 fun add_case thm thy =
   let
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/element.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -456,11 +456,16 @@
 
 fun eq_morphism _ [] = NONE
   | eq_morphism thy thms =
-      SOME (Morphism.morphism "Element.eq_morphism"
-       {binding = [],
-        typ = [],
-        term = [Raw_Simplifier.rewrite_term thy thms []],
-        fact = [map (rewrite_rule thms)]});
+      let
+        (* FIXME proper context!? *)
+        fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
+        val phi =
+          Morphism.morphism "Element.eq_morphism"
+           {binding = [],
+            typ = [],
+            term = [Raw_Simplifier.rewrite_term thy thms []],
+            fact = [map rewrite]};
+      in SOME phi end;
 
 
 
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/expression.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -619,7 +619,7 @@
     val bodyT = Term.fastype_of body;
   in
     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
-    else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
+    else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
   end;
 
 (* achieve plain syntax for locale predicates (without "PROP") *)
@@ -669,20 +669,22 @@
 
     val cert = Thm.cterm_of defs_thy;
 
-    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
-      rewrite_goals_tac [pred_def] THEN
-      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
-      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+    val intro = Goal.prove_global defs_thy [] norm_ts statement
+      (fn {context = ctxt, ...} =>
+        rewrite_goals_tac ctxt [pred_def] THEN
+        compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+        compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
-      (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
+      (Drule.equal_elim_rule2 OF
+        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_balanced (length ts);
 
     val (_, axioms_ctxt) = defs_ctxt
       |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness axioms_ctxt t
-       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
+       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 in
@@ -849,7 +851,7 @@
     val dep_morphs = map2 (fn (dep, morph) => fn wits =>
       (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
     fun activate' dep_morph ctxt = activate dep_morph
-      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
+        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
   in
     ctxt'
     |> fold activate' dep_morphs
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -104,7 +104,7 @@
     (*result*)
     val def =
       Thm.transitive local_def global_def
-      |> Local_Defs.contract defs
+      |> Local_Defs.contract lthy3 defs
           (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
     val ([(res_name, [res])], lthy4) = lthy3
       |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
@@ -125,7 +125,7 @@
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
-    val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
+    val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
@@ -153,7 +153,7 @@
     val result'' =
       (fold (curry op COMP) asms' result'
         handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
-      |> Local_Defs.contract defs (Thm.cprop_of th)
+      |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
       |> Goal.norm_result
       |> Global_Theory.name_thm false false name;
 
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/local_defs.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -17,7 +17,7 @@
     (term * term) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
   val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm
-  val contract: thm list -> cterm -> thm -> thm
+  val contract: Proof.context -> thm list -> cterm -> thm -> thm
   val print_rules: Proof.context -> unit
   val defn_add: attribute
   val defn_del: attribute
@@ -162,8 +162,8 @@
 fun export_cterm inner outer ct =
   export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
 
-fun contract defs ct th =
-  th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2);
+fun contract ctxt defs ct th =
+  th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2);
 
 
 
@@ -200,7 +200,7 @@
 
 (* rewriting with object-level rules *)
 
-fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
+fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt);
 
 val unfold       = meta Raw_Simplifier.rewrite_rule;
 val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
@@ -220,10 +220,12 @@
       |> conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt);
     fun prove ctxt' def =
-      Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop (K (ALLGOALS
-        (CONVERSION (meta_rewrite_conv ctxt') THEN'
-          rewrite_goal_tac [def] THEN'
-          resolve_tac [Drule.reflexive_thm])))
+      Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop
+        (fn {context = ctxt'', ...} =>
+          ALLGOALS
+            (CONVERSION (meta_rewrite_conv ctxt'') THEN'
+              rewrite_goal_tac ctxt'' [def] THEN'
+              resolve_tac [Drule.reflexive_thm]))
       handle ERROR msg => cat_error msg "Failed to prove definitional specification";
   in (((c, T), rhs), prove) end;
 
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/method.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -25,7 +25,7 @@
   val elim: thm list -> method
   val unfold: thm list -> Proof.context -> method
   val fold: thm list -> Proof.context -> method
-  val atomize: bool -> method
+  val atomize: bool -> Proof.context -> method
   val this: method
   val fact: thm list -> Proof.context -> method
   val assm_tac: Proof.context -> int -> tactic
@@ -33,14 +33,14 @@
   val assumption: Proof.context -> method
   val rule_trace: bool Config.T
   val trace: Proof.context -> thm list -> unit
-  val rule_tac: thm list -> thm list -> int -> tactic
-  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
+  val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
+  val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
   val intros_tac: thm list -> thm list -> tactic
   val try_intros_tac: thm list -> thm list -> tactic
-  val rule: thm list -> method
-  val erule: int -> thm list -> method
-  val drule: int -> thm list -> method
-  val frule: int -> thm list -> method
+  val rule: Proof.context -> thm list -> method
+  val erule: Proof.context -> int -> thm list -> method
+  val drule: Proof.context -> int -> thm list -> method
+  val frule: Proof.context -> int -> thm list -> method
   val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
   val tactic: string * Position.T -> Proof.context -> method
   val raw_tactic: string * Position.T -> Proof.context -> method
@@ -147,8 +147,10 @@
 
 (* atomize rule statements *)
 
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
-  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
+fun atomize false ctxt =
+      SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
+  | atomize true ctxt =
+      RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
 
 
 (* this -- resolve facts directly *)
@@ -159,7 +161,7 @@
 (* fact -- composition by facts from context *)
 
 fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
-  | fact rules _ = SIMPLE_METHOD' (Proof_Context.fact_tac rules);
+  | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
 
 
 (* assumption *)
@@ -208,31 +210,31 @@
 
 local
 
-fun gen_rule_tac tac rules facts =
+fun gen_rule_tac tac ctxt rules facts =
   (fn i => fn st =>
     if null facts then tac rules i st
     else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
-  THEN_ALL_NEW Goal.norm_hhf_tac;
+  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
 
-fun gen_arule_tac tac j rules facts =
-  EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
+fun gen_arule_tac tac ctxt j rules facts =
+  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
 
-fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
+fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
   let
     val rules =
       if not (null arg_rules) then arg_rules
       else flat (Context_Rules.find_rules false facts goal ctxt)
-  in trace ctxt rules; tac rules facts i end);
+  in trace ctxt rules; tac ctxt rules facts i end);
 
-fun meth tac x = METHOD (HEADGOAL o tac x);
-fun meth' tac x y = METHOD (HEADGOAL o tac x y);
+fun meth tac x y = METHOD (HEADGOAL o tac x y);
+fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
 
 in
 
 val rule_tac = gen_rule_tac resolve_tac;
 val rule = meth rule_tac;
 val some_rule_tac = gen_some_rule_tac rule_tac;
-val some_rule = meth' some_rule_tac;
+val some_rule = meth some_rule_tac;
 
 val erule = meth' (gen_arule_tac eresolve_tac);
 val drule = meth' (gen_arule_tac dresolve_tac);
@@ -390,9 +392,9 @@
 
 (* extra rule methods *)
 
-fun xrule_meth m =
+fun xrule_meth meth =
   Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
-  (fn (n, ths) => K (m n ths));
+  (fn (n, ths) => fn ctxt => meth ctxt n ths);
 
 
 (* outer parser *)
@@ -451,9 +453,10 @@
     "repeatedly apply elimination rules" #>
   setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
   setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
-  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
+  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
     "present local premises as object-level statements" #>
-  setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
+  setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
+    "apply some intro/elim rule" #>
   setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
   setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
   setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/object_logic.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -21,14 +21,14 @@
   val declare_atomize: attribute
   val declare_rulify: attribute
   val atomize_term: theory -> term -> term
-  val atomize: conv
-  val atomize_prems: conv
-  val atomize_prems_tac: int -> tactic
-  val full_atomize_tac: int -> tactic
+  val atomize: Proof.context -> conv
+  val atomize_prems: Proof.context -> conv
+  val atomize_prems_tac: Proof.context -> int -> tactic
+  val full_atomize_tac: Proof.context -> int -> tactic
   val rulify_term: theory -> term -> term
-  val rulify_tac: int -> tactic
-  val rulify: thm -> thm
-  val rulify_no_asm: thm -> thm
+  val rulify_tac: Proof.context -> int -> tactic
+  val rulify: Proof.context -> thm -> thm
+  val rulify_no_asm: Proof.context -> thm -> thm
   val rule_format: attribute
   val rule_format_no_asm: attribute
 end;
@@ -182,32 +182,31 @@
 fun atomize_term thy =
   drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
 
-fun atomize ct =
-  Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
+fun atomize ctxt =
+  Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
 
-fun atomize_prems ct =
+fun atomize_prems ctxt ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
-    Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
-      (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
+    Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize) ctxt ct
   else Conv.all_conv ct;
 
-val atomize_prems_tac = CONVERSION atomize_prems;
-val full_atomize_tac = CONVERSION atomize;
+val atomize_prems_tac = CONVERSION o atomize_prems;
+val full_atomize_tac = CONVERSION o atomize;
 
 
 (* rulify *)
 
 fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
+fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
 
-fun gen_rulify full thm =
-  Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm
-  |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
+fun gen_rulify full ctxt =
+  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
+  #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
 
 val rulify = gen_rulify true;
 val rulify_no_asm = gen_rulify false;
 
-val rule_format = Thm.rule_attribute (K rulify);
-val rule_format_no_asm = Thm.rule_attribute (K rulify_no_asm);
+val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
+val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
 
 end;
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/proof.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -443,18 +443,18 @@
 
 local
 
-fun finish_tac 0 = K all_tac
-  | finish_tac n =
-      Goal.norm_hhf_tac THEN'
+fun finish_tac _ 0 = K all_tac
+  | finish_tac ctxt n =
+      Goal.norm_hhf_tac ctxt THEN'
       SUBGOAL (fn (goal, i) =>
         if can Logic.unprotect (Logic.strip_assums_concl goal) then
-          etac Drule.protectI i THEN finish_tac (n - 1) i
-        else finish_tac (n - 1) (i + 1));
+          etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
+        else finish_tac ctxt (n - 1) (i + 1));
 
-fun goal_tac rule =
-  Goal.norm_hhf_tac THEN'
+fun goal_tac ctxt rule =
+  Goal.norm_hhf_tac ctxt THEN'
   rtac rule THEN'
-  finish_tac (Thm.nprems_of rule);
+  finish_tac ctxt (Thm.nprems_of rule);
 
 fun FINDGOAL tac st =
   let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
@@ -465,7 +465,7 @@
 fun refine_goals print_rule inner raw_rules state =
   let
     val (outer, (_, goal)) = get_goal state;
-    fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
+    fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
   in
     raw_rules
     |> Proof_Context.goal_export inner outer
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/proof_context.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -110,7 +110,7 @@
     (term list list * (Proof.context -> Proof.context)) * Proof.context
   val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
     (term list list * (Proof.context -> Proof.context)) * Proof.context
-  val fact_tac: thm list -> int -> tactic
+  val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
@@ -889,12 +889,12 @@
 
 in
 
-fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
+fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts;
 
 fun potential_facts ctxt prop =
   Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
 
-fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
+fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
 
 end;
 
@@ -913,7 +913,7 @@
 
         val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
         fun prove_fact th =
-          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
+          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
         val results = map_filter (try prove_fact) (potential_facts ctxt prop');
         val res =
           (case distinct Thm.eq_thm_prop results of
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/rule_cases.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -31,7 +31,7 @@
   val make_nested: term -> theory * term ->
     ((string * string list) * string list) list -> cases
   val apply: term list -> T -> T
-  val consume: thm list -> thm list -> ('a * int) * thm ->
+  val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
   val get_consumes: thm -> int
   val put_consumes: int option -> thm -> thm
@@ -203,24 +203,24 @@
 
 local
 
-fun unfold_prems n defs th =
+fun unfold_prems ctxt n defs th =
   if null defs then th
-  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
+  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th;
 
-fun unfold_prems_concls defs th =
+fun unfold_prems_concls ctxt defs th =
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   else
     Conv.fconv_rule
       (Conv.concl_conv ~1 (Conjunction.convs
-        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
+        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th;
 
 in
 
-fun consume defs facts ((xx, n), th) =
+fun consume ctxt defs facts ((xx, n), th) =
   let val m = Int.min (length facts, n) in
     th
-    |> unfold_prems n defs
-    |> unfold_prems_concls defs
+    |> unfold_prems ctxt n defs
+    |> unfold_prems_concls ctxt defs
     |> Drule.multi_resolve (take m facts)
     |> Seq.map (pair (xx, (n - m, drop m facts)))
   end;
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Tools/find_theorems.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -237,7 +237,9 @@
       Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal'
-      else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
+      else
+        (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
+          1 goal';
   in
     fn Internal (_, thm) =>
         if is_some (Seq.pull (try_thm thm))
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/axclass.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -291,11 +291,17 @@
 
 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
 
-fun unoverload thy = rewrite_rule (inst_thms thy);
-fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy));
+fun unoverload thy =
+  rewrite_rule (Proof_Context.init_global thy) (inst_thms thy);
+
+fun overload thy =
+  rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy));
 
-fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
-fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
+fun unoverload_conv thy =
+  Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy);
+
+fun overload_conv thy =
+  Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy));
 
 fun lookup_inst_param consts params (c, T) =
   (case get_inst_tyco consts (c, T) of
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/goal.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -49,7 +49,7 @@
   val conjunction_tac: int -> tactic
   val precise_conjunction_tac: int -> int -> tactic
   val recover_conjunction_tac: tactic
-  val norm_hhf_tac: int -> tactic
+  val norm_hhf_tac: Proof.context -> int -> tactic
   val assume_rule_tac: Proof.context -> int -> tactic
 end;
 
@@ -317,11 +317,11 @@
 
 (* hhf normal form *)
 
-val norm_hhf_tac =
+fun norm_hhf_tac ctxt =
   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   THEN' SUBGOAL (fn (t, i) =>
     if Drule.is_norm_hhf t then all_tac
-    else rewrite_goal_tac Drule.norm_hhf_eqs i);
+    else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
 
 
 (* non-atomic goal assumptions *)
@@ -330,7 +330,7 @@
   | non_atomic (Const ("all", _) $ _) = true
   | non_atomic _ = false;
 
-fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
+fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
   let
     val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
diff -r 7068557b7c63 -r 283fc522d24e src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/raw_simplifier.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -57,13 +57,13 @@
   val setSolver: Proof.context * solver -> Proof.context
   val addSolver: Proof.context * solver -> Proof.context
 
-  val rewrite_rule: thm list -> thm -> thm
-  val rewrite_goals_rule: thm list -> thm -> thm
-  val rewrite_goals_tac: thm list -> tactic
-  val rewrite_goal_tac: thm list -> int -> tactic
-  val prune_params_tac: tactic
-  val fold_rule: thm list -> thm -> thm
-  val fold_goals_tac: thm list -> tactic
+  val rewrite_rule: Proof.context -> thm list -> thm -> thm
+  val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
+  val rewrite_goals_tac: Proof.context -> thm list -> tactic
+  val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
+  val prune_params_tac: Proof.context -> tactic
+  val fold_rule: Proof.context -> thm list -> thm -> thm
+  val fold_goals_tac: Proof.context -> thm list -> tactic
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
 end;
@@ -126,7 +126,7 @@
     (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
   val generic_rewrite_goal_tac: bool * bool * bool ->
     (Proof.context -> tactic) -> Proof.context -> int -> tactic
-  val rewrite: bool -> thm list -> conv
+  val rewrite: Proof.context -> bool -> thm list -> conv
 end;
 
 structure Raw_Simplifier: RAW_SIMPLIFIER =
@@ -1366,12 +1366,12 @@
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
 
-fun rewrite _ [] ct = Thm.reflexive ct
-  | rewrite full thms ct =
+fun rewrite _ _ [] = Thm.reflexive
+  | rewrite ctxt full thms =
       rewrite_cterm (full, false, false) simple_prover
-        (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+        (empty_simpset ctxt addsimps thms);
 
-val rewrite_rule = Conv.fconv_rule o rewrite true;
+fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
 
 (*simple term rewriting -- no proof*)
 fun rewrite_term thy rules procs =
@@ -1380,15 +1380,15 @@
 fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
 
 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
-fun rewrite_goals_rule thms th =
+fun rewrite_goals_rule ctxt thms th =
   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
-    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+    (empty_simpset ctxt addsimps thms))) th;
 
 
 (** meta-rewriting tactics **)
 
 (*Rewrite all subgoals*)
-fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
+fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
 
 (*Rewrite one subgoal*)
 fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
@@ -1396,12 +1396,12 @@
     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
   else Seq.empty;
 
-fun rewrite_goal_tac rews i st =
+fun rewrite_goal_tac ctxt rews =
   generic_rewrite_goal_tac (true, false, false) (K no_tac)
-    (global_context (Thm.theory_of_thm st) empty_ss addsimps rews) i st;
+    (empty_simpset ctxt addsimps rews);
 
 (*Prunes all redundant parameters from the proof state by rewriting.*)
-val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
+fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
 
 
 (* for folding definitions, handling critical pairs *)
@@ -1422,8 +1422,8 @@
 
 val rev_defs = sort_lhs_depths o map Thm.symmetric;
 
-fun fold_rule defs = fold rewrite_rule (rev_defs defs);
-fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
+fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
+fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
 
 
 (* HHF normal form: !! before ==>, outermost !! generalized *)
diff -r 7068557b7c63 -r 283fc522d24e src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/S4.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -43,7 +43,8 @@
 )
 *}
 
-method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *}
+method_setup S4_solve =
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2)) *}
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 7068557b7c63 -r 283fc522d24e src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/S43.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -90,8 +90,8 @@
 
 
 method_setup S43_solve = {*
-  Scan.succeed (K (SIMPLE_METHOD
-    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
+  Scan.succeed (fn ctxt => SIMPLE_METHOD
+    (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3))
 *}
 
 
diff -r 7068557b7c63 -r 283fc522d24e src/Sequents/T.thy
--- a/src/Sequents/T.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/T.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -42,7 +42,7 @@
 )
 *}
 
-method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
+method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *}
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 7068557b7c63 -r 283fc522d24e src/Sequents/modal.ML
--- a/src/Sequents/modal.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/modal.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -19,7 +19,7 @@
     val rule_tac   : thm list -> int ->tactic
     val step_tac   : int -> tactic
     val solven_tac : int -> int -> tactic
-    val solve_tac  : int -> tactic
+    val solve_tac  : Proof.context -> int -> tactic
 end;
 
 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
@@ -78,7 +78,7 @@
                  ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
                    (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
 
-fun solve_tac d = rewrite_goals_tac Modal_Rule.rewrite_rls THEN solven_tac d 1;
+fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
 
 fun step_tac n = 
     COND (has_fewer_prems 1) all_tac 
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/atomize_elim.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -59,8 +59,8 @@
    (EX x y z. ...) | ... | (EX a b c. ...)
 *)
 fun atomize_elim_conv ctxt ct =
-    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
-    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
+    (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
+    then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
     then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/case_product.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -65,14 +65,14 @@
     (concl, prems)
   end
 
-fun case_product_tac prems struc thm1 thm2 =
+fun case_product_tac ctxt prems struc thm1 thm2 =
   let
     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
     val thm2' = thm2 OF p_cons2
   in
     rtac (thm1 OF p_cons1)
      THEN' EVERY' (map (fn p =>
-       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
+       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
   end
 
 fun combine ctxt thm1 thm2 =
@@ -80,8 +80,9 @@
     val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
     val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
   in
-    Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
-      case_product_tac prems prems_rich i_thm1 i_thm2 1)
+    Goal.prove ctxt' [] (flat prems_rich) concl
+      (fn {context = ctxt'', prems} =>
+        case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1)
     |> singleton (Variable.export ctxt' ctxt)
   end
 
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/coherent.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -41,14 +41,14 @@
 
 val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
 
-fun rulify_elim_conv ct =
+fun rulify_elim_conv ctxt ct =
   if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
   else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
     (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
-     Raw_Simplifier.rewrite true (map Thm.symmetric
+     Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
 
-fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
+fun rulify_elim ctxt th = Simplifier.norm_hhf (Conv.fconv_rule (rulify_elim_conv ctxt) th);
 
 (* Decompose elimination rule of the form
    A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
@@ -66,9 +66,9 @@
        (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
   end;
 
-fun mk_rule th =
+fun mk_rule ctxt th =
   let
-    val th' = rulify_elim th;
+    val th' = rulify_elim ctxt th;
     val (prems, cases) = dest_elim (prop_of th')
   in (th', prems, cases) end;
 
@@ -208,19 +208,19 @@
 
 (** external interface **)
 
-fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
-  rtac (rulify_elim_conv concl RS Drule.equal_elim_rule2) 1 THEN
-  SUBPROOF (fn {prems = prems', concl, context, ...} =>
+fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
+  rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
+  SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
     let val xs = map (term_of o #2) params @
-      map (fn (_, s) => Free (s, the (Variable.default_type context s)))
-        (rev (Variable.dest_fixes context))  (* FIXME !? *)
+      map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
+        (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
     in
-      case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
+      case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
            (mk_dom xs) Net.empty 0 0 of
          NONE => no_tac
        | SOME prf =>
-           rtac (thm_of_cl_prf (Proof_Context.theory_of context) concl [] prf) 1
-    end) context 1) ctxt;
+           rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
+    end) ctxt' 1) ctxt;
 
 val setup = Method.setup @{binding coherent}
   (Attrib.thms >> (fn rules => fn ctxt =>
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/eqsubst.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -328,7 +328,7 @@
     val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
     val preelimrule =
       RW_Inst.rw ctxt m rule pth
-      |> (Seq.hd o prune_params_tac)
+      |> (Seq.hd o prune_params_tac ctxt)
       |> Thm.permute_prems 0 ~1 (* put old asm first *)
       |> unfix_frees cfvs (* unfix any global params *)
       |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/induct.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -60,16 +60,16 @@
   val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
     (term option list * thm list) * Proof.context
   val atomize_term: theory -> term -> term
-  val atomize_cterm: conv
-  val atomize_tac: int -> tactic
-  val inner_atomize_tac: int -> tactic
+  val atomize_cterm: Proof.context -> conv
+  val atomize_tac: Proof.context -> int -> tactic
+  val inner_atomize_tac: Proof.context -> int -> tactic
   val rulified_term: thm -> theory * term
-  val rulify_tac: int -> tactic
+  val rulify_tac: Proof.context -> int -> tactic
   val simplified_rule: Proof.context -> thm -> thm
   val simplify_tac: Proof.context -> int -> tactic
   val trivial_tac: int -> tactic
   val rotate_tac: int -> int -> int -> tactic
-  val internalize: int -> thm -> thm
+  val internalize: Proof.context -> int -> thm -> thm
   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
@@ -433,10 +433,10 @@
 
 fun mark_constraints n ctxt = Conv.fconv_rule
   (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
-     (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
+     (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
 
-val unmark_constraints = Conv.fconv_rule
-  (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
+fun unmark_constraints ctxt =
+  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
 
 
 (* simplify *)
@@ -504,11 +504,11 @@
   in
     fn i => fn st =>
       ruleq
-      |> Seq.maps (Rule_Cases.consume [] facts)
+      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         let
           val rule' = rule
-            |> simp ? (simplified_rule' ctxt #> unmark_constraints);
+            |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
         in
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
@@ -532,12 +532,12 @@
   Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
   #> Object_Logic.drop_judgment thy;
 
-val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
+fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
 
-val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
+fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
 
-val inner_atomize_tac =
-  rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
+fun inner_atomize_tac ctxt =
+  rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt;
 
 
 (* rulify *)
@@ -553,11 +553,11 @@
     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
-val rulify_tac =
-  rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
-  rewrite_goal_tac Induct_Args.rulify_fallback THEN'
+fun rulify_tac ctxt =
+  rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
+  rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
   Goal.conjunction_tac THEN_ALL_NEW
-  (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
+  (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
 
 
 (* prepare rule *)
@@ -565,9 +565,9 @@
 fun rule_instance ctxt inst rule =
   Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
 
-fun internalize k th =
+fun internalize ctxt k th =
   th |> Thm.permute_prems 0 k
-  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
+  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt));
 
 
 (* guess rule instantiation -- cannot handle pending goal parameters *)
@@ -683,8 +683,10 @@
     | NONE => all_tac)
   end);
 
-fun miniscope_tac p = CONVERSION o
-  Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
+fun miniscope_tac p =
+  CONVERSION o
+    Conv.params_conv p (fn ctxt =>
+      Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
 
 in
 
@@ -743,7 +745,7 @@
     val thy = Proof_Context.theory_of ctxt;
 
     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
+    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
 
     fun inst_rule (concls, r) =
       (if null insts then `Rule_Cases.get r
@@ -774,7 +776,7 @@
   in
     (fn i => fn st =>
       ruleq
-      |> Seq.maps (Rule_Cases.consume (flat defs) facts)
+      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
@@ -791,9 +793,9 @@
                  else
                    arbitrary_tac defs_ctxt k xs)
              end)
-          THEN' inner_atomize_tac) j))
-        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
-            guess_instance ctxt (internalize more_consumes rule) i st'
+          THEN' inner_atomize_tac defs_ctxt) j))
+        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
             |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
@@ -802,7 +804,7 @@
     THEN_ALL_NEW_CASES
       ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
         else K all_tac)
-       THEN_ALL_NEW rulify_tac)
+       THEN_ALL_NEW rulify_tac ctxt)
   end;
 
 val induct_tac = gen_induct_tac (K I);
@@ -849,7 +851,7 @@
   in
     SUBGOAL_CASES (fn (goal, i) => fn st =>
       ruleq goal
-      |> Seq.maps (Rule_Cases.consume [] facts)
+      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         guess_instance ctxt rule i st
         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/induct_tacs.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -98,7 +98,7 @@
             (_, rule) :: _ => rule
           | [] => raise THM ("No induction rules", 0, [])));
 
-    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
+    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
     val _ = Method.trace ctxt [rule'];
 
     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
diff -r 7068557b7c63 -r 283fc522d24e src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/intuitionistic.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -89,7 +89,7 @@
   Method.setup name
     (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
       (fn opt_lim => fn ctxt =>
-        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
+        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
     "intuitionistic proof search";
 
 end;
diff -r 7068557b7c63 -r 283fc522d24e src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/cartprod.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -51,9 +51,9 @@
   val mk_prod : typ * typ -> typ
   val mk_tuple : term -> typ -> term list -> term
   val pseudo_type : term -> typ
-  val remove_split : thm -> thm
+  val remove_split : Proof.context -> thm -> thm
   val split_const : typ -> term
-  val split_rule_var : term * typ * thm -> thm
+  val split_rule_var : Proof.context -> term * typ * thm -> thm
   end;
 
 
@@ -100,18 +100,18 @@
   | mk_tuple pair T (t::_) = t;
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [Pr.split_eq];
+fun remove_split ctxt = rewrite_rule ctxt [Pr.split_eq];
 
 (*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
-fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
+fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
       let val T' = factors T1 ---> T2
           val newt = ap_split T1 T2 (Var(v,T'))
           val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
       in
-          remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
+          remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
                                            cterm newt)]) rl)
       end
-  | split_rule_var (t,T,rl) = rl;
+  | split_rule_var _ (t,T,rl) = rl;
 
 end;
 
diff -r 7068557b7c63 -r 283fc522d24e src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/datatype_package.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -288,8 +288,8 @@
     Goal.prove_global thy1 [] []
       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
-      (fn _ => EVERY
-        [rewrite_goals_tac [con_def],
+      (fn {context = ctxt, ...} => EVERY
+        [rewrite_goals_tac ctxt [con_def],
          rtac case_trans 1,
          REPEAT
            (resolve_tac [@{thm refl}, split_trans,
@@ -353,9 +353,9 @@
       val ctxt = Proof_Context.init_global thy;
     in
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
-        (fn _ => EVERY
-         [rewrite_goals_tac con_defs,
-          fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
+        (fn {context = ctxt', ...} => EVERY
+         [rewrite_goals_tac ctxt' con_defs,
+          fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])
     end;
 
   val simps = case_eqns @ recursor_eqns;
diff -r 7068557b7c63 -r 283fc522d24e src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/ind_cases.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -58,7 +58,7 @@
 val setup =
   Method.setup @{binding "ind_cases"}
     (Scan.lift (Scan.repeat1 Args.name_source) >>
-      (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
+      (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
     "dynamic case analysis on sets";
 
 
diff -r 7068557b7c63 -r 283fc522d24e src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/inductive_package.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -214,7 +214,7 @@
 
   (*Type-checking is hardest aspect of proof;
     disjIn selects the correct disjunct after unfolding*)
-  fun intro_tacsf disjIn =
+  fun intro_tacsf disjIn ctxt =
     [DETERM (stac unfold 1),
      REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
      (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
@@ -223,7 +223,7 @@
        backtracking may occur if the premises have extra variables!*)
      DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
      (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
-     rewrite_goals_tac con_defs,
+     rewrite_goals_tac ctxt con_defs,
      REPEAT (rtac @{thm refl} 2),
      (*Typechecking; this can fail*)
      if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
@@ -246,7 +246,7 @@
     (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
     |> ListPair.map (fn (t, tacs) =>
       Goal.prove_global thy1 [] [] t
-        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
+        (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt)));
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";
@@ -255,9 +255,9 @@
   fun basic_elim_tac ctxt =
       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
                 ORELSE' bound_hyp_subst_tac ctxt))
-      THEN prune_params_tac
+      THEN prune_params_tac ctxt
           (*Mutual recursion: collapse references to Part(D,h)*)
-      THEN (PRIMITIVE (fold_rule part_rec_defs));
+      THEN (PRIMITIVE (fold_rule ctxt part_rec_defs));
 
   (*Elimination*)
   val elim =
@@ -337,8 +337,8 @@
      val quant_induct =
        Goal.prove_global thy1 [] ind_prems
          (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
-         (fn {prems, ...} => EVERY
-           [rewrite_goals_tac part_rec_defs,
+         (fn {context = ctxt, prems} => EVERY
+           [rewrite_goals_tac ctxt part_rec_defs,
             rtac (@{thm impI} RS @{thm allI}) 1,
             DETERM (etac raw_induct 1),
             (*Push Part inside Collect*)
@@ -349,7 +349,7 @@
               some premise involves disjunction.*)
             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
                                ORELSE' (bound_hyp_subst_tac ctxt1))),
-            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
+            ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
 
      val dummy =
       if ! Ind_Syntax.trace then
@@ -422,9 +422,9 @@
           (writeln "  Proving the mutual induction rule...";
            Goal.prove_global thy1 [] []
              (Logic.mk_implies (induct_concl, mutual_induct_concl))
-             (fn _ => EVERY
-               [rewrite_goals_tac part_rec_defs,
-                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
+             (fn {context = ctxt, ...} => EVERY
+               [rewrite_goals_tac ctxt part_rec_defs,
+                REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac 1)]))
        else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
 
      val dummy =
@@ -452,15 +452,15 @@
                    RLN (2,[@{thm rev_subsetD}]);
 
      (*Minimizes backtracking by delivering the correct premise to each goal*)
-     fun mutual_ind_tac [] 0 = all_tac
-       | mutual_ind_tac(prem::prems) i =
+     fun mutual_ind_tac _ [] 0 = all_tac
+       | mutual_ind_tac ctxt (prem::prems) i =
            DETERM
             (SELECT_GOAL
                (
                 (*Simplify the assumptions and goal by unfolding Part and
                   using freeness of the Sum constructors; proves all but one
                   conjunct by contradiction*)
-                rewrite_goals_tac all_defs  THEN
+                rewrite_goals_tac ctxt all_defs  THEN
                 simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1  THEN
                 IF_UNSOLVED (*simp_tac may have finished it off!*)
                   ((*simplify assumptions*)
@@ -471,20 +471,20 @@
                    THEN
                    (*unpackage and use "prem" in the corresponding place*)
                    REPEAT (rtac @{thm impI} 1)  THEN
-                   rtac (rewrite_rule all_defs prem) 1  THEN
+                   rtac (rewrite_rule ctxt all_defs prem) 1  THEN
                    (*prem must not be REPEATed below: could loop!*)
                    DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
                                            eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
                ) i)
-            THEN mutual_ind_tac prems (i-1);
+            THEN mutual_ind_tac ctxt prems (i-1);
 
      val mutual_induct_fsplit =
        if need_mutual then
          Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
            mutual_induct_concl
-           (fn {prems, ...} => EVERY
+           (fn {context = ctxt, prems} => EVERY
              [rtac (quant_induct RS lemma) 1,
-              mutual_ind_tac (rev prems) (length prems)])
+              mutual_ind_tac ctxt (rev prems) (length prems)])
        else @{thm TrueI};
 
      (** Uncurrying the predicate in the ordinary induction rule **)
@@ -502,9 +502,11 @@
 
      val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
 
-     val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
-                  |> Drule.export_without_context
-     and mutual_induct = CP.remove_split mutual_induct_fsplit
+     val induct =
+       CP.split_rule_var (Proof_Context.init_global thy)
+        (pred_var, elem_type-->FOLogic.oT, induct0)
+       |> Drule.export_without_context
+     and mutual_induct = CP.remove_split (Proof_Context.init_global thy) mutual_induct_fsplit
 
      val ([induct', mutual_induct'], thy') =
        thy
diff -r 7068557b7c63 -r 283fc522d24e src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/primrec_package.ML	Sun Dec 15 05:11:46 2013 +0100
@@ -176,7 +176,7 @@
     val eqn_thms =
       eqn_terms |> map (fn t =>
         Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
-          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
+          (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
 
     val (eqn_thms', thy2) =
       thy1
diff -r 7068557b7c63 -r 283fc522d24e src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/UNITY/Constrains.thy	Sun Dec 15 05:11:46 2013 +0100
@@ -479,7 +479,7 @@
                                    @{thm constrains_imp_Constrains}] 1),
               rtac @{thm constrainsI} 1,
               (* Three subgoals *)
-              rewrite_goal_tac [@{thm st_set_def}] 3,
+              rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
               REPEAT (force_tac ctxt 2),
               full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
               ALLGOALS (clarify_tac ctxt),