# HG changeset patch
# User wenzelm
# Date 1388496556 -3600
# Node ID dd04a8b654fc03b2f57174eba085edc12672b815
# Parent  61276a7fc3690e76b9d9f6f251b75c86600e8794
proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

diff -r 61276a7fc369 -r dd04a8b654fc src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy	Tue Dec 31 14:29:16 2013 +0100
@@ -1075,12 +1075,12 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\
+  @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given
+  \item @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given
   theorem according to the canonical form specified above.  This is
   occasionally helpful to repair some low-level tools that do not
   handle Hereditary Harrop Formulae properly.
diff -r 61276a7fc369 -r dd04a8b654fc src/Doc/IsarImplementation/Proof.thy
--- a/src/Doc/IsarImplementation/Proof.thy	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Doc/IsarImplementation/Proof.thy	Tue Dec 31 14:29:16 2013 +0100
@@ -279,7 +279,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type Assumption.export} \\
-  @{index_ML Assumption.assume: "cterm -> thm"} \\
+  @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\
   @{index_ML Assumption.add_assms:
     "Assumption.export ->
   cterm list -> Proof.context -> thm list * Proof.context"} \\
@@ -296,7 +296,7 @@
   and the @{ML_type "cterm list"} the collection of assumptions to be
   discharged simultaneously.
 
-  \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
+  \item @{ML Assumption.assume}~@{text "ctxt A"} turns proposition @{text
   "A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the
   conclusion @{text "A'"} is in HHF normal form.
 
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -1215,7 +1215,7 @@
 val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
   lthy
   |> Proof.theorem NONE after_qed goalss
-  |> Proof.refine (Method.primitive_text I)
+  |> Proof.refine (Method.primitive_text (K I))
   |> Seq.hd) ooo add_primcorec_ursive_cmd NONE;
 
 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -143,7 +143,7 @@
           tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
   in th
     |> singleton (Proof_Context.export ctxt3 ctxt)
-    |> Goal.norm_result
+    |> Goal.norm_result ctxt
   end
 
 end
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Probability/measurable.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -153,9 +153,8 @@
 
 fun measurable_tac' ctxt facts =
   let
-
     val imported_thms =
-      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
+      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_all ctxt
 
     fun debug_facts msg () =
       msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -111,7 +111,7 @@
       (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
 
     val thm =
-      Goal.prove_internal (map cert prems) (cert concl)
+      Goal.prove_internal ctxt (map cert prems) (cert concl)
         (fn prems =>
            EVERY [
             rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -161,6 +161,7 @@
 
 fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype.info) thy =
   let
+    val ctxt = Proof_Context.init_global thy;
     val cert = cterm_of thy;
     val rT = TFree ("'P", HOLogic.typeS);
     val rT' = TVar (("'P", 0), HOLogic.typeS);
@@ -188,7 +189,7 @@
     val y' = Free ("y", T);
 
     val thm =
-      Goal.prove_internal (map cert prems)
+      Goal.prove_internal ctxt (map cert prems)
         (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
         (fn prems =>
            EVERY [
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -166,7 +166,7 @@
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
+    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
   end
 
 val function =
@@ -252,7 +252,7 @@
        [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
     |> Proof_Context.note_thmss ""
        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
-         [([Goal.norm_result termination], [])])] |> snd
+         [([Goal.norm_result lthy termination], [])])] |> snd
     |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
   end
 
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -116,7 +116,7 @@
    val js = subtract (op =) is (0 upto (length xs) - 1)
    val ty = fastype_of t
  in
-   Goal.prove_internal []
+   Goal.prove_internal ctxt []
      (cterm_of thy
        (Logic.mk_equals (t,
           if null is
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -265,7 +265,7 @@
       |> HOLogic.mk_Trueprop
       |> Logic.all x_uc;
 
-    val mono_thm = Goal.prove_internal [] (cert mono_goal)
+    val mono_thm = Goal.prove_internal lthy [] (cert mono_goal)
         (K (mono_tac lthy 1))
     val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
 
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -214,7 +214,7 @@
       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
+    Goal.prove_internal ctxt [ex_tm] conc tacf
     |> forall_intr_list frees
     |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
     |> Thm.varifyT_global
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -64,7 +64,7 @@
     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
+  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
 
 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
   | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
@@ -101,7 +101,7 @@
          so that "Thm.equal_elim" works below. *)
       val t0 $ _ $ t2 = prop_of eq_th
       val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
-      val eq_th' = Goal.prove_internal [] eq_ct (K (rtac eq_th 1))
+      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (rtac eq_th 1))
     in Thm.equal_elim eq_th' th end
 
 fun clause_params ordering =
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -738,7 +738,7 @@
       if ntac then no_tac
       else
         (case try (fn () =>
-            Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
+            Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
           NONE => no_tac
         | SOME r => rtac r i)
     end)
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -480,7 +480,7 @@
       val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
       val tac =
         Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1
-    in Goal.norm_result (Goal.prove_internal [] eq (K tac)) end
+    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
 
   fun ite_conv cv1 cv2 =
     Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -7,7 +7,7 @@
 signature Z3_PROOF_METHODS =
 sig
   val prove_injectivity: Proof.context -> cterm -> thm
-  val prove_ite: cterm -> thm
+  val prove_ite: Proof.context -> cterm -> thm
 end
 
 structure Z3_Proof_Methods: Z3_PROOF_METHODS =
@@ -30,8 +30,8 @@
   (Conv.rewr_conv pull_ite then_conv
    Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
 
-val prove_ite =
-  Z3_Proof_Tools.by_tac (
+fun prove_ite ctxt =
+  Z3_Proof_Tools.by_tac ctxt (
     CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
     THEN' rtac @{thm refl})
 
@@ -68,17 +68,17 @@
 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 ctxt (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})
     |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
-    |> Goal.norm_result o Goal.finish ctxt'
+    |> Goal.norm_result ctxt' o Goal.finish ctxt'
     |> singleton (Variable.export ctxt' ctxt)
   end
 
 fun prove_rhs ctxt def lhs =
-  Z3_Proof_Tools.by_tac (
+  Z3_Proof_Tools.by_tac ctxt (
     CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
     THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
     THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
@@ -97,7 +97,7 @@
     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 (
+    Z3_Proof_Tools.by_tac ctxt (
       CONVERSION (SMT_Utils.prop_conv conv)
       THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt))
   end
@@ -140,7 +140,7 @@
 in
 
 fun prove_injectivity ctxt =
-  Z3_Proof_Tools.by_tac (
+  Z3_Proof_Tools.by_tac ctxt (
     CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
     THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
 
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -315,7 +315,7 @@
 
 (* distributivity of | over & *)
 fun distributivity ctxt = Thm o try_apply ctxt [] [
-  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
+  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
     (* FIXME: not very well tested *)
 
 
@@ -371,7 +371,7 @@
 fun def_axiom ctxt = Thm o try_apply ctxt [] [
   named ctxt "conj/disj/distinct" prove_def_axiom,
   Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
-    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
+    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))]
 end
 
 
@@ -425,23 +425,23 @@
   fun nnf_quant_tac_varified vars eq =
     nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
 
-  fun nnf_quant vars qs p ct =
+  fun nnf_quant ctxt vars qs p ct =
     Z3_Proof_Tools.as_meta_eq ct
-    |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
+    |> Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
 
   fun prove_nnf ctxt = try_apply ctxt [] [
     named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
     Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
-      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
+      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))]
 in
 fun nnf ctxt vars ps ct =
   (case SMT_Utils.term_of ct of
     _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
       if l aconv r
       then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
-      else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
+      else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct)
   | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
-      MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
+      MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct)
   | _ =>
       let
         val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
@@ -555,25 +555,25 @@
     @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
     @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
 in
-fun quant_intro vars p ct =
+fun quant_intro ctxt vars p ct =
   let
     val thm = meta_eq_of p
     val rules' = Z3_Proof_Tools.varify vars thm :: rules
     val cu = Z3_Proof_Tools.as_meta_eq ct
     val tac = REPEAT_ALL_NEW (match_tac rules')
-  in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
+  in MetaEq (Z3_Proof_Tools.by_tac ctxt tac cu) end
 end
 
 
 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
 fun pull_quant ctxt = Thm o try_apply ctxt [] [
-  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
+  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
     (* FIXME: not very well tested *)
 
 
 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
 fun push_quant ctxt = Thm o try_apply ctxt [] [
-  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
+  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
     (* FIXME: not very well tested *)
 
 
@@ -590,14 +590,14 @@
       THEN' elim_unused_tac)) i st
 in
 
-val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac
+fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac ctxt elim_unused_tac
 
 end
 
 
 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
-  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
+  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
     (* FIXME: not very well tested *)
 
 
@@ -605,7 +605,7 @@
 local
   val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
 in
-val quant_inst = Thm o Z3_Proof_Tools.by_tac (
+fun quant_inst ctxt = Thm o Z3_Proof_Tools.by_tac ctxt (
   REPEAT_ALL_NEW (match_tac [rule])
   THEN' rtac @{thm excluded_middle})
 end
@@ -656,7 +656,7 @@
 (* theory lemmas: linear arithmetic, arrays *)
 fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
   Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
-    Z3_Proof_Tools.by_tac (
+    Z3_Proof_Tools.by_tac ctxt' (
       NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
       ORELSE' NAMED ctxt' "simp+arith" (
         Simplifier.asm_full_simp_tac (put_simpset simpset ctxt')
@@ -716,20 +716,20 @@
 fun rewrite simpset ths ct ctxt =
   apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
     named ctxt "conj/disj/distinct" prove_conj_disj_eq,
-    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
+    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite ctxt,
     Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
-      Z3_Proof_Tools.by_tac (
+      Z3_Proof_Tools.by_tac ctxt' (
         NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
         THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
     Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
-      Z3_Proof_Tools.by_tac (
+      Z3_Proof_Tools.by_tac ctxt' (
         (rtac @{thm iff_allI} ORELSE' K all_tac)
         THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
         THEN_ALL_NEW (
           NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
           ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
     Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
-      Z3_Proof_Tools.by_tac (
+      Z3_Proof_Tools.by_tac ctxt' (
         (rtac @{thm iff_allI} ORELSE' K all_tac)
         THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
         THEN_ALL_NEW (
@@ -738,7 +738,7 @@
     named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt),
     Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
       (fn ctxt' =>
-        Z3_Proof_Tools.by_tac (
+        Z3_Proof_Tools.by_tac ctxt' (
           (rtac @{thm iff_allI} ORELSE' K all_tac)
           THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
           THEN_ALL_NEW (
@@ -815,12 +815,12 @@
     | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
 
       (* quantifier rules *)
-    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
+    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp)
     | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
     | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
-    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp)
+    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
     | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
-    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
+    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp)
     | (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
 
       (* theory rules *)
@@ -861,17 +861,17 @@
   fun discharge_assms_tac rules =
     REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
     
-  fun discharge_assms rules thm =
-    if Thm.nprems_of thm = 0 then Goal.norm_result thm
+  fun discharge_assms ctxt rules thm =
+    if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
     else
       (case Seq.pull (discharge_assms_tac rules thm) of
-        SOME (thm', _) => Goal.norm_result thm'
+        SOME (thm', _) => Goal.norm_result ctxt thm'
       | NONE => raise THM ("failed to discharge premise", 1, [thm]))
 
   fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
     thm_of p
     |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
-    |> discharge_assms (make_discharge_rules rules)
+    |> discharge_assms outer_ctxt (make_discharge_rules rules)
 in
 
 fun reconstruct outer_ctxt recon output =
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -21,7 +21,7 @@
   val varify: string list -> thm -> thm
   val unfold_eqs: Proof.context -> thm list -> conv
   val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
-  val by_tac: (int -> tactic) -> cterm -> thm
+  val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm
   val make_hyp_def: thm -> Proof.context -> thm * Proof.context
   val by_abstraction: int -> bool * bool -> Proof.context -> thm list ->
     (Proof.context -> cterm -> thm) -> cterm -> thm
@@ -105,7 +105,7 @@
 fun match_instantiate f ct thm =
   Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
 
-fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
+fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1)))
 
 (*
    |- c x == t x ==> P (c x)
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -357,7 +357,7 @@
   hol_simplify ctxt inductive_conj
   #> hol_simplify ctxt inductive_rulify
   #> hol_simplify ctxt inductive_rulify_fallback
-  #> Simplifier.norm_hhf;
+  #> Simplifier.norm_hhf ctxt;
 
 end;
 
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/transfer.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -637,12 +637,12 @@
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
             THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
-    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
+    val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
   in
     thm3
       |> Raw_Simplifier.rewrite_rule ctxt' post_simps
-      |> Raw_Simplifier.norm_hhf
+      |> Simplifier.norm_hhf ctxt'
       |> Drule.generalize (tnames, [])
       |> Drule.zero_var_indexes
   end
@@ -673,12 +673,12 @@
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
             THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
-    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
+    val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
   in
     thm3
       |> Raw_Simplifier.rewrite_rule ctxt' post_simps
-      |> Raw_Simplifier.norm_hhf
+      |> Simplifier.norm_hhf ctxt'
       |> Drule.generalize (tnames, [])
       |> Drule.zero_var_indexes
   end
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/typedef.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -185,7 +185,7 @@
       let
         val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
         val typedef' = inhabited RS typedef;
-        fun make th = Goal.norm_result (typedef' RS th);
+        fun make th = Goal.norm_result lthy1 (typedef' RS th);
         val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
             Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
           |> Local_Theory.note ((typedef_name, []), [typedef'])
@@ -239,7 +239,7 @@
       prepare_typedef Syntax.check_term typ set opt_morphs lthy;
     val inhabited =
       Goal.prove lthy' [] [] goal (K tac)
-      |> Goal.norm_result |> Thm.close_derivation;
+      |> Goal.norm_result lthy' |> Thm.close_derivation;
   in typedef_result inhabited lthy' end;
 
 fun add_typedef_global typ set opt_morphs tac =
diff -r 61276a7fc369 -r dd04a8b654fc src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Tue Dec 31 14:29:16 2013 +0100
@@ -517,7 +517,7 @@
                      |> Thm.apply @{cterm Trueprop};
       in
         try (fn () =>
-          Goal.prove_internal [] prop 
+          Goal.prove_internal ctxt [] prop 
             (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
                 ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
       end
@@ -535,7 +535,7 @@
         val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
         val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
                  |> Thm.apply @{cterm Trueprop};
-      in Goal.prove_internal [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
+      in Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
              |> mk_meta_eq |> SOME end
     handle TERM _ => NONE | TYPE _ => NONE)
   | _ => NONE;
@@ -561,14 +561,14 @@
     val _ = if arg = arg' then raise TERM ("", []) else ();
     fun propfn g = HOLogic.mk_eq (g arg, g arg')
       |> HOLogic.mk_Trueprop |> cterm_of thy;
-    val eq1 = Goal.prove_internal [] (propfn I)
+    val eq1 = Goal.prove_internal ctxt [] (propfn I)
       (K (simp_tac (put_simpset word_ss ctxt) 1));
-  in Goal.prove_internal [] (propfn (curry (op $) f))
+  in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
       (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
        |> mk_meta_eq |> SOME end
     handle TERM _ => NONE;
 
-fun nat_get_Suc_simproc n_sucs thy cts = Simplifier.make_simproc
+fun nat_get_Suc_simproc n_sucs cts = Simplifier.make_simproc
   {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts,
    name = "nat_get_Suc", identifier = [],
    proc = K (nat_get_Suc_simproc_fn n_sucs)};
@@ -601,7 +601,7 @@
                                 takefill_last_simps drop_nonempty_simps
                                 rev_bl_order_simps}
           addsimprocs [expand_upt_simproc,
-                       nat_get_Suc_simproc 4 @{theory}
+                       nat_get_Suc_simproc 4
                          [@{cpat replicate}, @{cpat "takefill ?x"},
                           @{cpat drop}, @{cpat "bin_to_bl"},
                           @{cpat "takefill_last ?x"},
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/class.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -379,7 +379,7 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val intros = (snd o rules thy) sup :: map_filter I
-      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_witn,
+      [Option.map (Drule.export_without_context_open o Element.conclude_witness lthy) some_witn,
         (fst o rules thy) sub];
     val classrel =
       Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -60,7 +60,7 @@
         val tac = loc_intro_tac
           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;
+    val some_axiom = Option.map (Element.conclude_witness empty_ctxt) some_witn;
 
     (* canonical interpretation *)
     val base_morph = inst_morph
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/element.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -44,7 +44,7 @@
     string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
     Proof.state
   val transform_witness: morphism -> witness -> witness
-  val conclude_witness: witness -> thm
+  val conclude_witness: Proof.context -> witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
   val instT_morphism: theory -> typ Symtab.table -> morphism
   val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
@@ -223,7 +223,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
+    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf ctxt raw_th);
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
@@ -316,8 +316,8 @@
         (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
   end;
 
-fun conclude_witness (Witness (_, th)) =
-  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
+fun conclude_witness ctxt (Witness (_, th)) =
+  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
 
 fun pretty_witness ctxt witn =
   let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -693,7 +693,8 @@
 
 fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
   let
-    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
+    val ctxt = Proof_Context.init_global thy;
+    val defs' = map (cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
 
     val (a_pred, a_intro, a_axioms, thy'') =
       if null exts then (NONE, NONE, [], thy)
@@ -717,13 +718,15 @@
           val ((statement, intro, axioms), thy''') =
             thy''
             |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
+          val ctxt''' = Proof_Context.init_global thy''';
           val (_, thy'''') =
             thy'''
             |> Sign.qualified_path true binding
             |> Global_Theory.note_thmss ""
                  [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
                   ((Binding.conceal (Binding.name axiomsN), []),
-                    [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
+                    [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
+                      [])])]
             ||> Sign.restore_naming thy''';
         in (SOME statement, SOME intro, axioms, thy'''') end;
   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
@@ -740,9 +743,9 @@
       |> apfst (curry Notes "")
   | assumes_to_notes e axms = (e, axms);
 
-fun defines_to_notes thy (Defines defs) =
+fun defines_to_notes ctxt (Defines defs) =
       Notes ("", map (fn (a, (def, _)) =>
-        (a, [([Assumption.assume (cterm_of thy def)],
+        (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
@@ -770,6 +773,7 @@
       else raw_predicate_binding;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
       define_preds predicate_binding parms text thy;
+    val pred_ctxt = Proof_Context.init_global thy';
 
     val a_satisfy = Element.satisfy_morphism a_axioms;
     val b_satisfy = Element.satisfy_morphism b_axioms;
@@ -782,20 +786,21 @@
     val notes =
       if is_some asm then
         [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
-          [([Assumption.assume (cterm_of thy' (the asm))],
+          [([Assumption.assume pred_ctxt (cterm_of thy' (the asm))],
             [(Attrib.internal o K) Locale.witness_add])])])]
       else [];
 
     val notes' = body_elems |>
-      map (defines_to_notes thy') |>
+      map (defines_to_notes pred_ctxt) |>
       map (Element.transform_ctxt a_satisfy) |>
-      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
+      (fn elems =>
+        fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |>
       fst |>
       map (Element.transform_ctxt b_satisfy) |>
       map_filter (fn Notes notes => SOME notes | _ => NONE);
 
     val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
-    val axioms = map Element.conclude_witness b_axioms;
+    val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
 
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -123,7 +123,7 @@
     val cert = Thm.cterm_of thy;
 
     (*export assumes/defines*)
-    val th = Goal.norm_result raw_th;
+    val th = Goal.norm_result ctxt raw_th;
     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
     val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
 
@@ -154,7 +154,7 @@
       (fold (curry op COMP) asms' result'
         handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
       |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
-      |> Goal.norm_result
+      |> Goal.norm_result ctxt
       |> Global_Theory.name_thm false false name;
 
   in (result'', result) end;
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/method.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -54,7 +54,7 @@
     Try of text |
     Repeat1 of text |
     Select_Goals of int * text
-  val primitive_text: (thm -> thm) -> text
+  val primitive_text: (Proof.context -> thm -> thm) -> text
   val succeed_text: text
   val default_text: text
   val this_text: text
@@ -293,7 +293,7 @@
   Repeat1 of text |
   Select_Goals of int * text;
 
-fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)));
+fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
 val succeed_text = Basic (K succeed);
 val default_text = Source (Args.src (("default", []), Position.none));
 val this_text = Basic (K this);
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -194,7 +194,8 @@
     val rule =
       (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
-      | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
+      | SOME th =>
+          check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
 
     val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
     val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
@@ -300,8 +301,10 @@
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
       Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
-    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
-        (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
+    val before_qed =
+      Method.primitive_text (fn ctxt =>
+        Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
+          (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
     fun after_qed [[_, res]] =
       Proof.end_block #> guess_context (check_result ctxt thesis res);
   in
@@ -311,8 +314,8 @@
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (pair o rpair I)
-      "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
-    |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
+      "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
+    |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (cert thesis))) |> Seq.hd
   end;
 
 in
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -762,7 +762,7 @@
 
 fun norm_export_morphism inner outer =
   export_morphism inner outer $>
-  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result;
+  Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer);
 
 
 
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -391,7 +391,8 @@
 
     fun after_qed' results goal_ctxt' =
       let
-        val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
+        val results' =
+          burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
         val (res, lthy') =
           if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
           else
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/ML/ml_thms.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -97,7 +97,7 @@
             val ctxt = Context.proof_of context;
 
             val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
-            val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
+            val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
             fun after_qed res goal_ctxt =
               Proof_Context.put_thms false (Auto_Bind.thisN,
                 SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/assumption.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -9,7 +9,7 @@
   type export = bool -> cterm list -> (thm -> thm) * (term -> term)
   val assume_export: export
   val presume_export: export
-  val assume: cterm -> thm
+  val assume: Proof.context -> cterm -> thm
   val all_assms_of: Proof.context -> cterm list
   val all_prems_of: Proof.context -> thm list
   val check_hyps: Proof.context -> thm -> thm
@@ -48,7 +48,7 @@
 *)
 fun presume_export _ = assume_export false;
 
-val assume = Raw_Simplifier.norm_hhf o Thm.assume;
+fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
 
 
 
@@ -97,10 +97,11 @@
 
 (* add assumptions *)
 
-fun add_assms export new_asms =
-  let val new_prems = map assume new_asms in
-    map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
-    pair new_prems
+fun add_assms export new_asms ctxt =
+  let val new_prems = map (assume ctxt) new_asms in
+    ctxt
+    |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
+    |> pair new_prems
   end;
 
 val add_assumes = add_assms assume_export;
@@ -109,9 +110,9 @@
 (* export *)
 
 fun export is_goal inner outer =
-  Raw_Simplifier.norm_hhf_protect #>
+  Raw_Simplifier.norm_hhf_protect inner #>
   fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
-  Raw_Simplifier.norm_hhf_protect;
+  Raw_Simplifier.norm_hhf_protect outer;
 
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/goal.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -23,12 +23,12 @@
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
-  val norm_result: thm -> thm
+  val norm_result: Proof.context -> thm -> thm
   val skip_proofs_enabled: unit -> bool
   val future_enabled: int -> bool
   val future_enabled_timing: Time.time -> bool
   val future_result: Proof.context -> thm future -> term -> thm
-  val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
+  val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
   val is_schematic: term -> bool
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
@@ -98,9 +98,9 @@
 
 (* normal form *)
 
-val norm_result =
+fun norm_result ctxt =
   Drule.flexflex_unique
-  #> Raw_Simplifier.norm_hhf_protect
+  #> Raw_Simplifier.norm_hhf_protect ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
 
@@ -166,8 +166,8 @@
 
 (* prove_internal -- minimal checks, no normalization of result! *)
 
-fun prove_internal casms cprop tac =
-  (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
+fun prove_internal ctxt casms cprop tac =
+  (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
     SOME th => Drule.implies_intr_list casms
       (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
   | NONE => error "Tactic failed");
@@ -336,7 +336,7 @@
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
-      etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -64,8 +64,8 @@
   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
+  val norm_hhf: Proof.context -> thm -> thm
+  val norm_hhf_protect: Proof.context -> thm -> thm
 end;
 
 signature RAW_SIMPLIFIER =
@@ -1430,12 +1430,11 @@
 
 local
 
-fun gen_norm_hhf ss th =
+fun gen_norm_hhf ss ctxt th =
   (if Drule.is_norm_hhf (Thm.prop_of th) then th
    else
     Conv.fconv_rule
-      (rewrite_cterm (true, false, false) (K (K NONE))
-        (global_context (Thm.theory_of_thm th) ss)) th)
+      (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
   |> Thm.adjust_maxidx_thm ~1
   |> Drule.gen_all;
 
diff -r 61276a7fc369 -r dd04a8b654fc src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/subgoal.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -31,7 +31,7 @@
 
 fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   let
-    val st = Simplifier.norm_hhf_protect raw_st;
+    val st = Simplifier.norm_hhf_protect ctxt raw_st;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
 
diff -r 61276a7fc369 -r dd04a8b654fc src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Tools/coherent.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -48,7 +48,7 @@
      Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
 
-fun rulify_elim ctxt th = Simplifier.norm_hhf (Conv.fconv_rule (rulify_elim_conv ctxt) th);
+fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th);
 
 (* Decompose elimination rule of the form
    A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P