proper context for norm_hhf and derived operations;
authorwenzelm
Tue Dec 31 14:29:16 2013 +0100 (2013-12-31)
changeset 54883dd04a8b654fc
parent 54882 61276a7fc369
child 54884 81b3194defe0
proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;
src/Doc/IsarImplementation/Logic.thy
src/Doc/IsarImplementation/Proof.thy
src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/Probability/measurable.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/z3_proof_methods.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/transfer.ML
src/HOL/Tools/typedef.ML
src/HOL/Word/WordBitwise.thy
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_thms.ML
src/Pure/assumption.ML
src/Pure/goal.ML
src/Pure/raw_simplifier.ML
src/Pure/subgoal.ML
src/Tools/coherent.ML
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Tue Dec 31 11:19:14 2013 +0100
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Tue Dec 31 14:29:16 2013 +0100
     1.3 @@ -1075,12 +1075,12 @@
     1.4  
     1.5  text %mlref {*
     1.6    \begin{mldecls}
     1.7 -  @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\
     1.8 +  @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\
     1.9    \end{mldecls}
    1.10  
    1.11    \begin{description}
    1.12  
    1.13 -  \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given
    1.14 +  \item @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given
    1.15    theorem according to the canonical form specified above.  This is
    1.16    occasionally helpful to repair some low-level tools that do not
    1.17    handle Hereditary Harrop Formulae properly.
     2.1 --- a/src/Doc/IsarImplementation/Proof.thy	Tue Dec 31 11:19:14 2013 +0100
     2.2 +++ b/src/Doc/IsarImplementation/Proof.thy	Tue Dec 31 14:29:16 2013 +0100
     2.3 @@ -279,7 +279,7 @@
     2.4  text %mlref {*
     2.5    \begin{mldecls}
     2.6    @{index_ML_type Assumption.export} \\
     2.7 -  @{index_ML Assumption.assume: "cterm -> thm"} \\
     2.8 +  @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\
     2.9    @{index_ML Assumption.add_assms:
    2.10      "Assumption.export ->
    2.11    cterm list -> Proof.context -> thm list * Proof.context"} \\
    2.12 @@ -296,7 +296,7 @@
    2.13    and the @{ML_type "cterm list"} the collection of assumptions to be
    2.14    discharged simultaneously.
    2.15  
    2.16 -  \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
    2.17 +  \item @{ML Assumption.assume}~@{text "ctxt A"} turns proposition @{text
    2.18    "A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the
    2.19    conclusion @{text "A'"} is in HHF normal form.
    2.20  
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Dec 31 11:19:14 2013 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Dec 31 14:29:16 2013 +0100
     3.3 @@ -1215,7 +1215,7 @@
     3.4  val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
     3.5    lthy
     3.6    |> Proof.theorem NONE after_qed goalss
     3.7 -  |> Proof.refine (Method.primitive_text I)
     3.8 +  |> Proof.refine (Method.primitive_text (K I))
     3.9    |> Seq.hd) ooo add_primcorec_ursive_cmd NONE;
    3.10  
    3.11  val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
     4.1 --- a/src/HOL/Library/simps_case_conv.ML	Tue Dec 31 11:19:14 2013 +0100
     4.2 +++ b/src/HOL/Library/simps_case_conv.ML	Tue Dec 31 14:29:16 2013 +0100
     4.3 @@ -143,7 +143,7 @@
     4.4            tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
     4.5    in th
     4.6      |> singleton (Proof_Context.export ctxt3 ctxt)
     4.7 -    |> Goal.norm_result
     4.8 +    |> Goal.norm_result ctxt
     4.9    end
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Probability/measurable.ML	Tue Dec 31 11:19:14 2013 +0100
     5.2 +++ b/src/HOL/Probability/measurable.ML	Tue Dec 31 14:29:16 2013 +0100
     5.3 @@ -153,9 +153,8 @@
     5.4  
     5.5  fun measurable_tac' ctxt facts =
     5.6    let
     5.7 -
     5.8      val imported_thms =
     5.9 -      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
    5.10 +      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_all ctxt
    5.11  
    5.12      fun debug_facts msg () =
    5.13        msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
     6.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Dec 31 11:19:14 2013 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Dec 31 14:29:16 2013 +0100
     6.3 @@ -111,7 +111,7 @@
     6.4        (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
     6.5  
     6.6      val thm =
     6.7 -      Goal.prove_internal (map cert prems) (cert concl)
     6.8 +      Goal.prove_internal ctxt (map cert prems) (cert concl)
     6.9          (fn prems =>
    6.10             EVERY [
    6.11              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
    6.12 @@ -161,6 +161,7 @@
    6.13  
    6.14  fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype.info) thy =
    6.15    let
    6.16 +    val ctxt = Proof_Context.init_global thy;
    6.17      val cert = cterm_of thy;
    6.18      val rT = TFree ("'P", HOLogic.typeS);
    6.19      val rT' = TVar (("'P", 0), HOLogic.typeS);
    6.20 @@ -188,7 +189,7 @@
    6.21      val y' = Free ("y", T);
    6.22  
    6.23      val thm =
    6.24 -      Goal.prove_internal (map cert prems)
    6.25 +      Goal.prove_internal ctxt (map cert prems)
    6.26          (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
    6.27          (fn prems =>
    6.28             EVERY [
     7.1 --- a/src/HOL/Tools/Function/function.ML	Tue Dec 31 11:19:14 2013 +0100
     7.2 +++ b/src/HOL/Tools/Function/function.ML	Tue Dec 31 14:29:16 2013 +0100
     7.3 @@ -166,7 +166,7 @@
     7.4    in
     7.5      lthy'
     7.6      |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
     7.7 -    |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
     7.8 +    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
     7.9    end
    7.10  
    7.11  val function =
    7.12 @@ -252,7 +252,7 @@
    7.13         [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    7.14      |> Proof_Context.note_thmss ""
    7.15         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
    7.16 -         [([Goal.norm_result termination], [])])] |> snd
    7.17 +         [([Goal.norm_result lthy termination], [])])] |> snd
    7.18      |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
    7.19    end
    7.20  
     8.1 --- a/src/HOL/Tools/Function/function_lib.ML	Tue Dec 31 11:19:14 2013 +0100
     8.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Tue Dec 31 14:29:16 2013 +0100
     8.3 @@ -116,7 +116,7 @@
     8.4     val js = subtract (op =) is (0 upto (length xs) - 1)
     8.5     val ty = fastype_of t
     8.6   in
     8.7 -   Goal.prove_internal []
     8.8 +   Goal.prove_internal ctxt []
     8.9       (cterm_of thy
    8.10         (Logic.mk_equals (t,
    8.11            if null is
     9.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Dec 31 11:19:14 2013 +0100
     9.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Dec 31 14:29:16 2013 +0100
     9.3 @@ -265,7 +265,7 @@
     9.4        |> HOLogic.mk_Trueprop
     9.5        |> Logic.all x_uc;
     9.6  
     9.7 -    val mono_thm = Goal.prove_internal [] (cert mono_goal)
     9.8 +    val mono_thm = Goal.prove_internal lthy [] (cert mono_goal)
     9.9          (K (mono_tac lthy 1))
    9.10      val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
    9.11  
    10.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Dec 31 11:19:14 2013 +0100
    10.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Dec 31 14:29:16 2013 +0100
    10.3 @@ -214,7 +214,7 @@
    10.4        THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
    10.5                   RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
    10.6    in
    10.7 -    Goal.prove_internal [ex_tm] conc tacf
    10.8 +    Goal.prove_internal ctxt [ex_tm] conc tacf
    10.9      |> forall_intr_list frees
   10.10      |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   10.11      |> Thm.varifyT_global
    11.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Dec 31 11:19:14 2013 +0100
    11.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Dec 31 14:29:16 2013 +0100
    11.3 @@ -64,7 +64,7 @@
    11.4      val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
    11.5      val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
    11.6      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    11.7 -  in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
    11.8 +  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
    11.9  
   11.10  fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
   11.11    | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
   11.12 @@ -101,7 +101,7 @@
   11.13           so that "Thm.equal_elim" works below. *)
   11.14        val t0 $ _ $ t2 = prop_of eq_th
   11.15        val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
   11.16 -      val eq_th' = Goal.prove_internal [] eq_ct (K (rtac eq_th 1))
   11.17 +      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (rtac eq_th 1))
   11.18      in Thm.equal_elim eq_th' th end
   11.19  
   11.20  fun clause_params ordering =
    12.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Dec 31 11:19:14 2013 +0100
    12.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Dec 31 14:29:16 2013 +0100
    12.3 @@ -738,7 +738,7 @@
    12.4        if ntac then no_tac
    12.5        else
    12.6          (case try (fn () =>
    12.7 -            Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
    12.8 +            Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
    12.9            NONE => no_tac
   12.10          | SOME r => rtac r i)
   12.11      end)
    13.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 31 11:19:14 2013 +0100
    13.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 31 14:29:16 2013 +0100
    13.3 @@ -480,7 +480,7 @@
    13.4        val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
    13.5        val tac =
    13.6          Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1
    13.7 -    in Goal.norm_result (Goal.prove_internal [] eq (K tac)) end
    13.8 +    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
    13.9  
   13.10    fun ite_conv cv1 cv2 =
   13.11      Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
    14.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Dec 31 11:19:14 2013 +0100
    14.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Dec 31 14:29:16 2013 +0100
    14.3 @@ -7,7 +7,7 @@
    14.4  signature Z3_PROOF_METHODS =
    14.5  sig
    14.6    val prove_injectivity: Proof.context -> cterm -> thm
    14.7 -  val prove_ite: cterm -> thm
    14.8 +  val prove_ite: Proof.context -> cterm -> thm
    14.9  end
   14.10  
   14.11  structure Z3_Proof_Methods: Z3_PROOF_METHODS =
   14.12 @@ -30,8 +30,8 @@
   14.13    (Conv.rewr_conv pull_ite then_conv
   14.14     Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
   14.15  
   14.16 -val prove_ite =
   14.17 -  Z3_Proof_Tools.by_tac (
   14.18 +fun prove_ite ctxt =
   14.19 +  Z3_Proof_Tools.by_tac ctxt (
   14.20      CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
   14.21      THEN' rtac @{thm refl})
   14.22  
   14.23 @@ -68,17 +68,17 @@
   14.24  fun prove_inj_prop ctxt def lhs =
   14.25    let
   14.26      val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
   14.27 -    val rule = disjE OF [Object_Logic.rulify ctxt (Thm.assume lhs)]
   14.28 +    val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)]
   14.29    in
   14.30      Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
   14.31      |> apply (rtac @{thm injI})
   14.32      |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
   14.33 -    |> Goal.norm_result o Goal.finish ctxt'
   14.34 +    |> Goal.norm_result ctxt' o Goal.finish ctxt'
   14.35      |> singleton (Variable.export ctxt' ctxt)
   14.36    end
   14.37  
   14.38  fun prove_rhs ctxt def lhs =
   14.39 -  Z3_Proof_Tools.by_tac (
   14.40 +  Z3_Proof_Tools.by_tac ctxt (
   14.41      CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
   14.42      THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
   14.43      THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
   14.44 @@ -97,7 +97,7 @@
   14.45      val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
   14.46      val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
   14.47    in
   14.48 -    Z3_Proof_Tools.by_tac (
   14.49 +    Z3_Proof_Tools.by_tac ctxt (
   14.50        CONVERSION (SMT_Utils.prop_conv conv)
   14.51        THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt))
   14.52    end
   14.53 @@ -140,7 +140,7 @@
   14.54  in
   14.55  
   14.56  fun prove_injectivity ctxt =
   14.57 -  Z3_Proof_Tools.by_tac (
   14.58 +  Z3_Proof_Tools.by_tac ctxt (
   14.59      CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
   14.60      THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
   14.61  
    15.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Dec 31 11:19:14 2013 +0100
    15.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Dec 31 14:29:16 2013 +0100
    15.3 @@ -315,7 +315,7 @@
    15.4  
    15.5  (* distributivity of | over & *)
    15.6  fun distributivity ctxt = Thm o try_apply ctxt [] [
    15.7 -  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
    15.8 +  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
    15.9      (* FIXME: not very well tested *)
   15.10  
   15.11  
   15.12 @@ -371,7 +371,7 @@
   15.13  fun def_axiom ctxt = Thm o try_apply ctxt [] [
   15.14    named ctxt "conj/disj/distinct" prove_def_axiom,
   15.15    Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
   15.16 -    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
   15.17 +    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))]
   15.18  end
   15.19  
   15.20  
   15.21 @@ -425,23 +425,23 @@
   15.22    fun nnf_quant_tac_varified vars eq =
   15.23      nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
   15.24  
   15.25 -  fun nnf_quant vars qs p ct =
   15.26 +  fun nnf_quant ctxt vars qs p ct =
   15.27      Z3_Proof_Tools.as_meta_eq ct
   15.28 -    |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
   15.29 +    |> Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
   15.30  
   15.31    fun prove_nnf ctxt = try_apply ctxt [] [
   15.32      named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
   15.33      Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
   15.34 -      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
   15.35 +      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))]
   15.36  in
   15.37  fun nnf ctxt vars ps ct =
   15.38    (case SMT_Utils.term_of ct of
   15.39      _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
   15.40        if l aconv r
   15.41        then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
   15.42 -      else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
   15.43 +      else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct)
   15.44    | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
   15.45 -      MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
   15.46 +      MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct)
   15.47    | _ =>
   15.48        let
   15.49          val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
   15.50 @@ -555,25 +555,25 @@
   15.51      @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
   15.52      @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
   15.53  in
   15.54 -fun quant_intro vars p ct =
   15.55 +fun quant_intro ctxt vars p ct =
   15.56    let
   15.57      val thm = meta_eq_of p
   15.58      val rules' = Z3_Proof_Tools.varify vars thm :: rules
   15.59      val cu = Z3_Proof_Tools.as_meta_eq ct
   15.60      val tac = REPEAT_ALL_NEW (match_tac rules')
   15.61 -  in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
   15.62 +  in MetaEq (Z3_Proof_Tools.by_tac ctxt tac cu) end
   15.63  end
   15.64  
   15.65  
   15.66  (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
   15.67  fun pull_quant ctxt = Thm o try_apply ctxt [] [
   15.68 -  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   15.69 +  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
   15.70      (* FIXME: not very well tested *)
   15.71  
   15.72  
   15.73  (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
   15.74  fun push_quant ctxt = Thm o try_apply ctxt [] [
   15.75 -  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   15.76 +  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
   15.77      (* FIXME: not very well tested *)
   15.78  
   15.79  
   15.80 @@ -590,14 +590,14 @@
   15.81        THEN' elim_unused_tac)) i st
   15.82  in
   15.83  
   15.84 -val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac
   15.85 +fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac ctxt elim_unused_tac
   15.86  
   15.87  end
   15.88  
   15.89  
   15.90  (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
   15.91  fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
   15.92 -  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   15.93 +  named ctxt "fast" (Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
   15.94      (* FIXME: not very well tested *)
   15.95  
   15.96  
   15.97 @@ -605,7 +605,7 @@
   15.98  local
   15.99    val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
  15.100  in
  15.101 -val quant_inst = Thm o Z3_Proof_Tools.by_tac (
  15.102 +fun quant_inst ctxt = Thm o Z3_Proof_Tools.by_tac ctxt (
  15.103    REPEAT_ALL_NEW (match_tac [rule])
  15.104    THEN' rtac @{thm excluded_middle})
  15.105  end
  15.106 @@ -656,7 +656,7 @@
  15.107  (* theory lemmas: linear arithmetic, arrays *)
  15.108  fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
  15.109    Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
  15.110 -    Z3_Proof_Tools.by_tac (
  15.111 +    Z3_Proof_Tools.by_tac ctxt' (
  15.112        NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
  15.113        ORELSE' NAMED ctxt' "simp+arith" (
  15.114          Simplifier.asm_full_simp_tac (put_simpset simpset ctxt')
  15.115 @@ -716,20 +716,20 @@
  15.116  fun rewrite simpset ths ct ctxt =
  15.117    apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
  15.118      named ctxt "conj/disj/distinct" prove_conj_disj_eq,
  15.119 -    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
  15.120 +    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite ctxt,
  15.121      Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
  15.122 -      Z3_Proof_Tools.by_tac (
  15.123 +      Z3_Proof_Tools.by_tac ctxt' (
  15.124          NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
  15.125          THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
  15.126      Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
  15.127 -      Z3_Proof_Tools.by_tac (
  15.128 +      Z3_Proof_Tools.by_tac ctxt' (
  15.129          (rtac @{thm iff_allI} ORELSE' K all_tac)
  15.130          THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
  15.131          THEN_ALL_NEW (
  15.132            NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
  15.133            ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
  15.134      Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
  15.135 -      Z3_Proof_Tools.by_tac (
  15.136 +      Z3_Proof_Tools.by_tac ctxt' (
  15.137          (rtac @{thm iff_allI} ORELSE' K all_tac)
  15.138          THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
  15.139          THEN_ALL_NEW (
  15.140 @@ -738,7 +738,7 @@
  15.141      named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt),
  15.142      Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
  15.143        (fn ctxt' =>
  15.144 -        Z3_Proof_Tools.by_tac (
  15.145 +        Z3_Proof_Tools.by_tac ctxt' (
  15.146            (rtac @{thm iff_allI} ORELSE' K all_tac)
  15.147            THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
  15.148            THEN_ALL_NEW (
  15.149 @@ -815,12 +815,12 @@
  15.150      | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
  15.151  
  15.152        (* quantifier rules *)
  15.153 -    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
  15.154 +    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp)
  15.155      | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
  15.156      | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
  15.157 -    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp)
  15.158 +    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
  15.159      | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
  15.160 -    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
  15.161 +    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp)
  15.162      | (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
  15.163  
  15.164        (* theory rules *)
  15.165 @@ -861,17 +861,17 @@
  15.166    fun discharge_assms_tac rules =
  15.167      REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
  15.168      
  15.169 -  fun discharge_assms rules thm =
  15.170 -    if Thm.nprems_of thm = 0 then Goal.norm_result thm
  15.171 +  fun discharge_assms ctxt rules thm =
  15.172 +    if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
  15.173      else
  15.174        (case Seq.pull (discharge_assms_tac rules thm) of
  15.175 -        SOME (thm', _) => Goal.norm_result thm'
  15.176 +        SOME (thm', _) => Goal.norm_result ctxt thm'
  15.177        | NONE => raise THM ("failed to discharge premise", 1, [thm]))
  15.178  
  15.179    fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
  15.180      thm_of p
  15.181      |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
  15.182 -    |> discharge_assms (make_discharge_rules rules)
  15.183 +    |> discharge_assms outer_ctxt (make_discharge_rules rules)
  15.184  in
  15.185  
  15.186  fun reconstruct outer_ctxt recon output =
    16.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Dec 31 11:19:14 2013 +0100
    16.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Dec 31 14:29:16 2013 +0100
    16.3 @@ -21,7 +21,7 @@
    16.4    val varify: string list -> thm -> thm
    16.5    val unfold_eqs: Proof.context -> thm list -> conv
    16.6    val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
    16.7 -  val by_tac: (int -> tactic) -> cterm -> thm
    16.8 +  val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm
    16.9    val make_hyp_def: thm -> Proof.context -> thm * Proof.context
   16.10    val by_abstraction: int -> bool * bool -> Proof.context -> thm list ->
   16.11      (Proof.context -> cterm -> thm) -> cterm -> thm
   16.12 @@ -105,7 +105,7 @@
   16.13  fun match_instantiate f ct thm =
   16.14    Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
   16.15  
   16.16 -fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
   16.17 +fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1)))
   16.18  
   16.19  (*
   16.20     |- c x == t x ==> P (c x)
    17.1 --- a/src/HOL/Tools/inductive.ML	Tue Dec 31 11:19:14 2013 +0100
    17.2 +++ b/src/HOL/Tools/inductive.ML	Tue Dec 31 14:29:16 2013 +0100
    17.3 @@ -357,7 +357,7 @@
    17.4    hol_simplify ctxt inductive_conj
    17.5    #> hol_simplify ctxt inductive_rulify
    17.6    #> hol_simplify ctxt inductive_rulify_fallback
    17.7 -  #> Simplifier.norm_hhf;
    17.8 +  #> Simplifier.norm_hhf ctxt;
    17.9  
   17.10  end;
   17.11  
    18.1 --- a/src/HOL/Tools/transfer.ML	Tue Dec 31 11:19:14 2013 +0100
    18.2 +++ b/src/HOL/Tools/transfer.ML	Tue Dec 31 14:29:16 2013 +0100
    18.3 @@ -637,12 +637,12 @@
    18.4            (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
    18.5              THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
    18.6          handle TERM (_, ts) => raise TERM (err_msg, ts)
    18.7 -    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
    18.8 +    val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
    18.9      val tnames = map (fst o dest_TFree o snd) instT
   18.10    in
   18.11      thm3
   18.12        |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   18.13 -      |> Raw_Simplifier.norm_hhf
   18.14 +      |> Simplifier.norm_hhf ctxt'
   18.15        |> Drule.generalize (tnames, [])
   18.16        |> Drule.zero_var_indexes
   18.17    end
   18.18 @@ -673,12 +673,12 @@
   18.19            (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
   18.20              THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
   18.21          handle TERM (_, ts) => raise TERM (err_msg, ts)
   18.22 -    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
   18.23 +    val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
   18.24      val tnames = map (fst o dest_TFree o snd) instT
   18.25    in
   18.26      thm3
   18.27        |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   18.28 -      |> Raw_Simplifier.norm_hhf
   18.29 +      |> Simplifier.norm_hhf ctxt'
   18.30        |> Drule.generalize (tnames, [])
   18.31        |> Drule.zero_var_indexes
   18.32    end
    19.1 --- a/src/HOL/Tools/typedef.ML	Tue Dec 31 11:19:14 2013 +0100
    19.2 +++ b/src/HOL/Tools/typedef.ML	Tue Dec 31 14:29:16 2013 +0100
    19.3 @@ -185,7 +185,7 @@
    19.4        let
    19.5          val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
    19.6          val typedef' = inhabited RS typedef;
    19.7 -        fun make th = Goal.norm_result (typedef' RS th);
    19.8 +        fun make th = Goal.norm_result lthy1 (typedef' RS th);
    19.9          val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
   19.10              Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
   19.11            |> Local_Theory.note ((typedef_name, []), [typedef'])
   19.12 @@ -239,7 +239,7 @@
   19.13        prepare_typedef Syntax.check_term typ set opt_morphs lthy;
   19.14      val inhabited =
   19.15        Goal.prove lthy' [] [] goal (K tac)
   19.16 -      |> Goal.norm_result |> Thm.close_derivation;
   19.17 +      |> Goal.norm_result lthy' |> Thm.close_derivation;
   19.18    in typedef_result inhabited lthy' end;
   19.19  
   19.20  fun add_typedef_global typ set opt_morphs tac =
    20.1 --- a/src/HOL/Word/WordBitwise.thy	Tue Dec 31 11:19:14 2013 +0100
    20.2 +++ b/src/HOL/Word/WordBitwise.thy	Tue Dec 31 14:29:16 2013 +0100
    20.3 @@ -517,7 +517,7 @@
    20.4                       |> Thm.apply @{cterm Trueprop};
    20.5        in
    20.6          try (fn () =>
    20.7 -          Goal.prove_internal [] prop 
    20.8 +          Goal.prove_internal ctxt [] prop 
    20.9              (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
   20.10                  ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
   20.11        end
   20.12 @@ -535,7 +535,7 @@
   20.13          val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
   20.14          val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
   20.15                   |> Thm.apply @{cterm Trueprop};
   20.16 -      in Goal.prove_internal [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
   20.17 +      in Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
   20.18               |> mk_meta_eq |> SOME end
   20.19      handle TERM _ => NONE | TYPE _ => NONE)
   20.20    | _ => NONE;
   20.21 @@ -561,14 +561,14 @@
   20.22      val _ = if arg = arg' then raise TERM ("", []) else ();
   20.23      fun propfn g = HOLogic.mk_eq (g arg, g arg')
   20.24        |> HOLogic.mk_Trueprop |> cterm_of thy;
   20.25 -    val eq1 = Goal.prove_internal [] (propfn I)
   20.26 +    val eq1 = Goal.prove_internal ctxt [] (propfn I)
   20.27        (K (simp_tac (put_simpset word_ss ctxt) 1));
   20.28 -  in Goal.prove_internal [] (propfn (curry (op $) f))
   20.29 +  in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
   20.30        (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
   20.31         |> mk_meta_eq |> SOME end
   20.32      handle TERM _ => NONE;
   20.33  
   20.34 -fun nat_get_Suc_simproc n_sucs thy cts = Simplifier.make_simproc
   20.35 +fun nat_get_Suc_simproc n_sucs cts = Simplifier.make_simproc
   20.36    {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts,
   20.37     name = "nat_get_Suc", identifier = [],
   20.38     proc = K (nat_get_Suc_simproc_fn n_sucs)};
   20.39 @@ -601,7 +601,7 @@
   20.40                                  takefill_last_simps drop_nonempty_simps
   20.41                                  rev_bl_order_simps}
   20.42            addsimprocs [expand_upt_simproc,
   20.43 -                       nat_get_Suc_simproc 4 @{theory}
   20.44 +                       nat_get_Suc_simproc 4
   20.45                           [@{cpat replicate}, @{cpat "takefill ?x"},
   20.46                            @{cpat drop}, @{cpat "bin_to_bl"},
   20.47                            @{cpat "takefill_last ?x"},
    21.1 --- a/src/Pure/Isar/class.ML	Tue Dec 31 11:19:14 2013 +0100
    21.2 +++ b/src/Pure/Isar/class.ML	Tue Dec 31 14:29:16 2013 +0100
    21.3 @@ -379,7 +379,7 @@
    21.4    let
    21.5      val thy = Proof_Context.theory_of lthy;
    21.6      val intros = (snd o rules thy) sup :: map_filter I
    21.7 -      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_witn,
    21.8 +      [Option.map (Drule.export_without_context_open o Element.conclude_witness lthy) some_witn,
    21.9          (fst o rules thy) sub];
   21.10      val classrel =
   21.11        Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
    22.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Dec 31 11:19:14 2013 +0100
    22.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Dec 31 14:29:16 2013 +0100
    22.3 @@ -60,7 +60,7 @@
    22.4          val tac = loc_intro_tac
    22.5            THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
    22.6        in Element.prove_witness empty_ctxt prop tac end) some_prop;
    22.7 -    val some_axiom = Option.map Element.conclude_witness some_witn;
    22.8 +    val some_axiom = Option.map (Element.conclude_witness empty_ctxt) some_witn;
    22.9  
   22.10      (* canonical interpretation *)
   22.11      val base_morph = inst_morph
    23.1 --- a/src/Pure/Isar/element.ML	Tue Dec 31 11:19:14 2013 +0100
    23.2 +++ b/src/Pure/Isar/element.ML	Tue Dec 31 14:29:16 2013 +0100
    23.3 @@ -44,7 +44,7 @@
    23.4      string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
    23.5      Proof.state
    23.6    val transform_witness: morphism -> witness -> witness
    23.7 -  val conclude_witness: witness -> thm
    23.8 +  val conclude_witness: Proof.context -> witness -> thm
    23.9    val pretty_witness: Proof.context -> witness -> Pretty.T
   23.10    val instT_morphism: theory -> typ Symtab.table -> morphism
   23.11    val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
   23.12 @@ -223,7 +223,7 @@
   23.13    let
   23.14      val thy = Proof_Context.theory_of ctxt;
   23.15  
   23.16 -    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
   23.17 +    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf ctxt raw_th);
   23.18      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
   23.19      val prop = Thm.prop_of th';
   23.20      val (prems, concl) = Logic.strip_horn prop;
   23.21 @@ -316,8 +316,8 @@
   23.22          (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
   23.23    end;
   23.24  
   23.25 -fun conclude_witness (Witness (_, th)) =
   23.26 -  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
   23.27 +fun conclude_witness ctxt (Witness (_, th)) =
   23.28 +  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
   23.29  
   23.30  fun pretty_witness ctxt witn =
   23.31    let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
    24.1 --- a/src/Pure/Isar/expression.ML	Tue Dec 31 11:19:14 2013 +0100
    24.2 +++ b/src/Pure/Isar/expression.ML	Tue Dec 31 14:29:16 2013 +0100
    24.3 @@ -693,7 +693,8 @@
    24.4  
    24.5  fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
    24.6    let
    24.7 -    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
    24.8 +    val ctxt = Proof_Context.init_global thy;
    24.9 +    val defs' = map (cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
   24.10  
   24.11      val (a_pred, a_intro, a_axioms, thy'') =
   24.12        if null exts then (NONE, NONE, [], thy)
   24.13 @@ -717,13 +718,15 @@
   24.14            val ((statement, intro, axioms), thy''') =
   24.15              thy''
   24.16              |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
   24.17 +          val ctxt''' = Proof_Context.init_global thy''';
   24.18            val (_, thy'''') =
   24.19              thy'''
   24.20              |> Sign.qualified_path true binding
   24.21              |> Global_Theory.note_thmss ""
   24.22                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
   24.23                    ((Binding.conceal (Binding.name axiomsN), []),
   24.24 -                    [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
   24.25 +                    [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
   24.26 +                      [])])]
   24.27              ||> Sign.restore_naming thy''';
   24.28          in (SOME statement, SOME intro, axioms, thy'''') end;
   24.29    in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
   24.30 @@ -740,9 +743,9 @@
   24.31        |> apfst (curry Notes "")
   24.32    | assumes_to_notes e axms = (e, axms);
   24.33  
   24.34 -fun defines_to_notes thy (Defines defs) =
   24.35 +fun defines_to_notes ctxt (Defines defs) =
   24.36        Notes ("", map (fn (a, (def, _)) =>
   24.37 -        (a, [([Assumption.assume (cterm_of thy def)],
   24.38 +        (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
   24.39            [(Attrib.internal o K) Locale.witness_add])])) defs)
   24.40    | defines_to_notes _ e = e;
   24.41  
   24.42 @@ -770,6 +773,7 @@
   24.43        else raw_predicate_binding;
   24.44      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   24.45        define_preds predicate_binding parms text thy;
   24.46 +    val pred_ctxt = Proof_Context.init_global thy';
   24.47  
   24.48      val a_satisfy = Element.satisfy_morphism a_axioms;
   24.49      val b_satisfy = Element.satisfy_morphism b_axioms;
   24.50 @@ -782,20 +786,21 @@
   24.51      val notes =
   24.52        if is_some asm then
   24.53          [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
   24.54 -          [([Assumption.assume (cterm_of thy' (the asm))],
   24.55 +          [([Assumption.assume pred_ctxt (cterm_of thy' (the asm))],
   24.56              [(Attrib.internal o K) Locale.witness_add])])])]
   24.57        else [];
   24.58  
   24.59      val notes' = body_elems |>
   24.60 -      map (defines_to_notes thy') |>
   24.61 +      map (defines_to_notes pred_ctxt) |>
   24.62        map (Element.transform_ctxt a_satisfy) |>
   24.63 -      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   24.64 +      (fn elems =>
   24.65 +        fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |>
   24.66        fst |>
   24.67        map (Element.transform_ctxt b_satisfy) |>
   24.68        map_filter (fn Notes notes => SOME notes | _ => NONE);
   24.69  
   24.70      val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
   24.71 -    val axioms = map Element.conclude_witness b_axioms;
   24.72 +    val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
   24.73  
   24.74      val loc_ctxt = thy'
   24.75        |> Locale.register_locale binding (extraTs, params)
    25.1 --- a/src/Pure/Isar/generic_target.ML	Tue Dec 31 11:19:14 2013 +0100
    25.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Dec 31 14:29:16 2013 +0100
    25.3 @@ -123,7 +123,7 @@
    25.4      val cert = Thm.cterm_of thy;
    25.5  
    25.6      (*export assumes/defines*)
    25.7 -    val th = Goal.norm_result raw_th;
    25.8 +    val th = Goal.norm_result ctxt raw_th;
    25.9      val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
   25.10      val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
   25.11  
   25.12 @@ -154,7 +154,7 @@
   25.13        (fold (curry op COMP) asms' result'
   25.14          handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
   25.15        |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
   25.16 -      |> Goal.norm_result
   25.17 +      |> Goal.norm_result ctxt
   25.18        |> Global_Theory.name_thm false false name;
   25.19  
   25.20    in (result'', result) end;
    26.1 --- a/src/Pure/Isar/method.ML	Tue Dec 31 11:19:14 2013 +0100
    26.2 +++ b/src/Pure/Isar/method.ML	Tue Dec 31 14:29:16 2013 +0100
    26.3 @@ -54,7 +54,7 @@
    26.4      Try of text |
    26.5      Repeat1 of text |
    26.6      Select_Goals of int * text
    26.7 -  val primitive_text: (thm -> thm) -> text
    26.8 +  val primitive_text: (Proof.context -> thm -> thm) -> text
    26.9    val succeed_text: text
   26.10    val default_text: text
   26.11    val this_text: text
   26.12 @@ -293,7 +293,7 @@
   26.13    Repeat1 of text |
   26.14    Select_Goals of int * text;
   26.15  
   26.16 -fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)));
   26.17 +fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
   26.18  val succeed_text = Basic (K succeed);
   26.19  val default_text = Source (Args.src (("default", []), Position.none));
   26.20  val this_text = Basic (K this);
    27.1 --- a/src/Pure/Isar/obtain.ML	Tue Dec 31 11:19:14 2013 +0100
    27.2 +++ b/src/Pure/Isar/obtain.ML	Tue Dec 31 14:29:16 2013 +0100
    27.3 @@ -194,7 +194,8 @@
    27.4      val rule =
    27.5        (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
    27.6          NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
    27.7 -      | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
    27.8 +      | SOME th =>
    27.9 +          check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
   27.10  
   27.11      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
   27.12      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
   27.13 @@ -300,8 +301,10 @@
   27.14      val goal = Var (("guess", 0), propT);
   27.15      fun print_result ctxt' (k, [(s, [_, th])]) =
   27.16        Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
   27.17 -    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
   27.18 -        (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   27.19 +    val before_qed =
   27.20 +      Method.primitive_text (fn ctxt =>
   27.21 +        Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
   27.22 +          (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
   27.23      fun after_qed [[_, res]] =
   27.24        Proof.end_block #> guess_context (check_result ctxt thesis res);
   27.25    in
   27.26 @@ -311,8 +314,8 @@
   27.27      |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
   27.28      |> Proof.chain_facts chain_facts
   27.29      |> Proof.local_goal print_result (K I) (pair o rpair I)
   27.30 -      "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
   27.31 -    |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   27.32 +      "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
   27.33 +    |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (cert thesis))) |> Seq.hd
   27.34    end;
   27.35  
   27.36  in
    28.1 --- a/src/Pure/Isar/proof_context.ML	Tue Dec 31 11:19:14 2013 +0100
    28.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Dec 31 14:29:16 2013 +0100
    28.3 @@ -762,7 +762,7 @@
    28.4  
    28.5  fun norm_export_morphism inner outer =
    28.6    export_morphism inner outer $>
    28.7 -  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result;
    28.8 +  Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer);
    28.9  
   28.10  
   28.11  
    29.1 --- a/src/Pure/Isar/specification.ML	Tue Dec 31 11:19:14 2013 +0100
    29.2 +++ b/src/Pure/Isar/specification.ML	Tue Dec 31 14:29:16 2013 +0100
    29.3 @@ -391,7 +391,8 @@
    29.4  
    29.5      fun after_qed' results goal_ctxt' =
    29.6        let
    29.7 -        val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
    29.8 +        val results' =
    29.9 +          burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
   29.10          val (res, lthy') =
   29.11            if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
   29.12            else
    30.1 --- a/src/Pure/ML/ml_thms.ML	Tue Dec 31 11:19:14 2013 +0100
    30.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Dec 31 14:29:16 2013 +0100
    30.3 @@ -97,7 +97,7 @@
    30.4              val ctxt = Context.proof_of context;
    30.5  
    30.6              val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    30.7 -            val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
    30.8 +            val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
    30.9              fun after_qed res goal_ctxt =
   30.10                Proof_Context.put_thms false (Auto_Bind.thisN,
   30.11                  SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
    31.1 --- a/src/Pure/assumption.ML	Tue Dec 31 11:19:14 2013 +0100
    31.2 +++ b/src/Pure/assumption.ML	Tue Dec 31 14:29:16 2013 +0100
    31.3 @@ -9,7 +9,7 @@
    31.4    type export = bool -> cterm list -> (thm -> thm) * (term -> term)
    31.5    val assume_export: export
    31.6    val presume_export: export
    31.7 -  val assume: cterm -> thm
    31.8 +  val assume: Proof.context -> cterm -> thm
    31.9    val all_assms_of: Proof.context -> cterm list
   31.10    val all_prems_of: Proof.context -> thm list
   31.11    val check_hyps: Proof.context -> thm -> thm
   31.12 @@ -48,7 +48,7 @@
   31.13  *)
   31.14  fun presume_export _ = assume_export false;
   31.15  
   31.16 -val assume = Raw_Simplifier.norm_hhf o Thm.assume;
   31.17 +fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
   31.18  
   31.19  
   31.20  
   31.21 @@ -97,10 +97,11 @@
   31.22  
   31.23  (* add assumptions *)
   31.24  
   31.25 -fun add_assms export new_asms =
   31.26 -  let val new_prems = map assume new_asms in
   31.27 -    map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
   31.28 -    pair new_prems
   31.29 +fun add_assms export new_asms ctxt =
   31.30 +  let val new_prems = map (assume ctxt) new_asms in
   31.31 +    ctxt
   31.32 +    |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
   31.33 +    |> pair new_prems
   31.34    end;
   31.35  
   31.36  val add_assumes = add_assms assume_export;
   31.37 @@ -109,9 +110,9 @@
   31.38  (* export *)
   31.39  
   31.40  fun export is_goal inner outer =
   31.41 -  Raw_Simplifier.norm_hhf_protect #>
   31.42 +  Raw_Simplifier.norm_hhf_protect inner #>
   31.43    fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
   31.44 -  Raw_Simplifier.norm_hhf_protect;
   31.45 +  Raw_Simplifier.norm_hhf_protect outer;
   31.46  
   31.47  fun export_term inner outer =
   31.48    fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
    32.1 --- a/src/Pure/goal.ML	Tue Dec 31 11:19:14 2013 +0100
    32.2 +++ b/src/Pure/goal.ML	Tue Dec 31 14:29:16 2013 +0100
    32.3 @@ -23,12 +23,12 @@
    32.4    val conclude: thm -> thm
    32.5    val check_finished: Proof.context -> thm -> thm
    32.6    val finish: Proof.context -> thm -> thm
    32.7 -  val norm_result: thm -> thm
    32.8 +  val norm_result: Proof.context -> thm -> thm
    32.9    val skip_proofs_enabled: unit -> bool
   32.10    val future_enabled: int -> bool
   32.11    val future_enabled_timing: Time.time -> bool
   32.12    val future_result: Proof.context -> thm future -> term -> thm
   32.13 -  val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   32.14 +  val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
   32.15    val is_schematic: term -> bool
   32.16    val prove_multi: Proof.context -> string list -> term list -> term list ->
   32.17      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   32.18 @@ -98,9 +98,9 @@
   32.19  
   32.20  (* normal form *)
   32.21  
   32.22 -val norm_result =
   32.23 +fun norm_result ctxt =
   32.24    Drule.flexflex_unique
   32.25 -  #> Raw_Simplifier.norm_hhf_protect
   32.26 +  #> Raw_Simplifier.norm_hhf_protect ctxt
   32.27    #> Thm.strip_shyps
   32.28    #> Drule.zero_var_indexes;
   32.29  
   32.30 @@ -166,8 +166,8 @@
   32.31  
   32.32  (* prove_internal -- minimal checks, no normalization of result! *)
   32.33  
   32.34 -fun prove_internal casms cprop tac =
   32.35 -  (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
   32.36 +fun prove_internal ctxt casms cprop tac =
   32.37 +  (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
   32.38      SOME th => Drule.implies_intr_list casms
   32.39        (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
   32.40    | NONE => error "Tactic failed");
   32.41 @@ -336,7 +336,7 @@
   32.42      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
   32.43      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
   32.44      val tacs = Rs |> map (fn R =>
   32.45 -      etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   32.46 +      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   32.47    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
   32.48  
   32.49  
    33.1 --- a/src/Pure/raw_simplifier.ML	Tue Dec 31 11:19:14 2013 +0100
    33.2 +++ b/src/Pure/raw_simplifier.ML	Tue Dec 31 14:29:16 2013 +0100
    33.3 @@ -64,8 +64,8 @@
    33.4    val prune_params_tac: Proof.context -> tactic
    33.5    val fold_rule: Proof.context -> thm list -> thm -> thm
    33.6    val fold_goals_tac: Proof.context -> thm list -> tactic
    33.7 -  val norm_hhf: thm -> thm
    33.8 -  val norm_hhf_protect: thm -> thm
    33.9 +  val norm_hhf: Proof.context -> thm -> thm
   33.10 +  val norm_hhf_protect: Proof.context -> thm -> thm
   33.11  end;
   33.12  
   33.13  signature RAW_SIMPLIFIER =
   33.14 @@ -1430,12 +1430,11 @@
   33.15  
   33.16  local
   33.17  
   33.18 -fun gen_norm_hhf ss th =
   33.19 +fun gen_norm_hhf ss ctxt th =
   33.20    (if Drule.is_norm_hhf (Thm.prop_of th) then th
   33.21     else
   33.22      Conv.fconv_rule
   33.23 -      (rewrite_cterm (true, false, false) (K (K NONE))
   33.24 -        (global_context (Thm.theory_of_thm th) ss)) th)
   33.25 +      (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
   33.26    |> Thm.adjust_maxidx_thm ~1
   33.27    |> Drule.gen_all;
   33.28  
    34.1 --- a/src/Pure/subgoal.ML	Tue Dec 31 11:19:14 2013 +0100
    34.2 +++ b/src/Pure/subgoal.ML	Tue Dec 31 14:29:16 2013 +0100
    34.3 @@ -31,7 +31,7 @@
    34.4  
    34.5  fun gen_focus (do_prems, do_concl) ctxt i raw_st =
    34.6    let
    34.7 -    val st = Simplifier.norm_hhf_protect raw_st;
    34.8 +    val st = Simplifier.norm_hhf_protect ctxt raw_st;
    34.9      val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
   34.10      val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
   34.11  
    35.1 --- a/src/Tools/coherent.ML	Tue Dec 31 11:19:14 2013 +0100
    35.2 +++ b/src/Tools/coherent.ML	Tue Dec 31 14:29:16 2013 +0100
    35.3 @@ -48,7 +48,7 @@
    35.4       Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
    35.5         [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
    35.6  
    35.7 -fun rulify_elim ctxt th = Simplifier.norm_hhf (Conv.fconv_rule (rulify_elim_conv ctxt) th);
    35.8 +fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th);
    35.9  
   35.10  (* Decompose elimination rule of the form
   35.11     A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P