proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
authorwenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 547427a86358a3c0b
parent 54741 010eefa0a4f3
child 54743 b9ae4a2f615b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
NEWS
src/CCL/CCL.thy
src/Doc/IsarImplementation/Eq.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_fp_n2m.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/BNF/Tools/bnf_tactics.ML
src/HOL/Bali/Example.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/NSA/transfer.ML
src/HOL/Nat.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/TLA/Action.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/TLA.thy
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Datatype/primrec.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/SMT/z3_proof_methods.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/coinduction.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/record.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/simpdata.ML
src/HOL/Tools/transfer.ML
src/HOL/Word/Word.thy
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/code.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Tools/find_theorems.ML
src/Pure/axclass.ML
src/Pure/goal.ML
src/Pure/raw_simplifier.ML
src/Sequents/S4.thy
src/Sequents/S43.thy
src/Sequents/T.thy
src/Sequents/modal.ML
src/Tools/atomize_elim.ML
src/Tools/case_product.ML
src/Tools/coherent.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
src/Tools/intuitionistic.ML
src/ZF/Tools/cartprod.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/UNITY/Constrains.thy
     1.1 --- a/NEWS	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/NEWS	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -115,6 +115,11 @@
     1.4  Note that 'ML_file' is the canonical command to load ML files into the
     1.5  formal context.
     1.6  
     1.7 +* Proper context for basic Simplifier operations: rewrite_rule,
     1.8 +rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
     1.9 +pass runtime Proof.context (and ensure that the simplified entity
    1.10 +actually belongs to it).
    1.11 +
    1.12  
    1.13  *** System ***
    1.14  
     2.1 --- a/src/CCL/CCL.thy	Fri Dec 13 23:53:02 2013 +0100
     2.2 +++ b/src/CCL/CCL.thy	Sat Dec 14 17:28:05 2013 +0100
     2.3 @@ -280,7 +280,7 @@
     2.4      fun mk_dstnct_thm rls s =
     2.5        Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
     2.6          (fn _ =>
     2.7 -          rewrite_goals_tac defs THEN
     2.8 +          rewrite_goals_tac ctxt defs THEN
     2.9            simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
    2.10    in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    2.11  
     3.1 --- a/src/Doc/IsarImplementation/Eq.thy	Fri Dec 13 23:53:02 2013 +0100
     3.2 +++ b/src/Doc/IsarImplementation/Eq.thy	Sat Dec 14 17:28:05 2013 +0100
     3.3 @@ -91,30 +91,30 @@
     3.4  
     3.5  text %mlref {*
     3.6    \begin{mldecls}
     3.7 -  @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\
     3.8 -  @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\
     3.9 -  @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
    3.10 -  @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
    3.11 -  @{index_ML fold_goals_tac: "thm list -> tactic"} \\
    3.12 +  @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
    3.13 +  @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
    3.14 +  @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
    3.15 +  @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
    3.16 +  @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
    3.17    \end{mldecls}
    3.18  
    3.19    \begin{description}
    3.20  
    3.21 -  \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole
    3.22 +  \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
    3.23    theorem by the given rules.
    3.24  
    3.25 -  \item @{ML rewrite_goals_rule}~@{text "rules thm"} rewrites the
    3.26 +  \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
    3.27    outer premises of the given theorem.  Interpreting the same as a
    3.28    goal state (\secref{sec:tactical-goals}) it means to rewrite all
    3.29    subgoals (in the same manner as @{ML rewrite_goals_tac}).
    3.30  
    3.31 -  \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
    3.32 +  \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
    3.33    @{text "i"} by the given rewrite rules.
    3.34  
    3.35 -  \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals
    3.36 +  \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
    3.37    by the given rewrite rules.
    3.38  
    3.39 -  \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML
    3.40 +  \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
    3.41    rewrite_goals_tac} with the symmetric form of each member of @{text
    3.42    "rules"}, re-ordered to fold longer expression first.  This supports
    3.43    to idea to fold primitive definitions that appear in expended form
     4.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Dec 13 23:53:02 2013 +0100
     4.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Sat Dec 14 17:28:05 2013 +0100
     4.3 @@ -590,10 +590,10 @@
     4.4        fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
     4.5      val expand_rels =
     4.6        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
     4.7 -    val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
     4.8 -    val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
     4.9 -    val unfold_rels = unfold_thms lthy rel_unfolds;
    4.10 -    val unfold_all = unfold_sets o unfold_maps o unfold_rels;
    4.11 +    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
    4.12 +    fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
    4.13 +    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
    4.14 +    fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
    4.15      val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
    4.16      val bnf_sets = map (expand_maps o expand_sets)
    4.17        (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
    4.18 @@ -627,7 +627,7 @@
    4.19        map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
    4.20  
    4.21      fun mk_tac thm {context = ctxt, prems = _} =
    4.22 -      (rtac (unfold_all thm) THEN'
    4.23 +      (rtac (unfold_all ctxt thm) THEN'
    4.24        SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
    4.25  
    4.26      val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
    4.27 @@ -638,7 +638,8 @@
    4.28  
    4.29      val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    4.30  
    4.31 -    fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    4.32 +    fun wit_tac {context = ctxt, prems = _} =
    4.33 +      mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
    4.34  
    4.35      val (bnf', lthy') =
    4.36        bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
     5.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Dec 13 23:53:02 2013 +0100
     5.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Dec 14 17:28:05 2013 +0100
     5.3 @@ -130,7 +130,7 @@
     5.4        REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
     5.5      EVERY [REPEAT_DETERM_N r
     5.6          (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
     5.7 -      if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
     5.8 +      if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
     5.9        mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
    5.10    end;
    5.11  
     6.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Dec 13 23:53:02 2013 +0100
     6.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Sat Dec 14 17:28:05 2013 +0100
     6.3 @@ -168,7 +168,7 @@
     6.4              cterm_instantiate_pos cts rel_xtor_co_induct_thm
     6.5              |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
     6.6              |> funpow (2 * n) (fn thm => thm RS spec)
     6.7 -            |> Conv.fconv_rule Object_Logic.atomize
     6.8 +            |> Conv.fconv_rule (Object_Logic.atomize lthy)
     6.9              |> funpow n (fn thm => thm RS mp)
    6.10            end);
    6.11  
     7.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Dec 13 23:53:02 2013 +0100
     7.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Dec 14 17:28:05 2013 +0100
     7.3 @@ -567,7 +567,7 @@
     7.4        EVERY' [rtac allI, fo_rtac induct ctxt,
     7.5          select_prem_tac n (dtac @{thm meta_spec2}) i,
     7.6          REPEAT_DETERM_N n o
     7.7 -          EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac,
     7.8 +          EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
     7.9              REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac],
    7.10          atac];
    7.11    in
     8.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Dec 13 23:53:02 2013 +0100
     8.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Sat Dec 14 17:28:05 2013 +0100
     8.3 @@ -45,7 +45,7 @@
     8.4      rtac (Drule.instantiate_normalize insts thm) 1
     8.5    end);
     8.6  
     8.7 -fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
     8.8 +fun mk_unfold_thms_then_tac ctxt defs tac x = unfold_thms_tac ctxt defs THEN tac x;
     8.9  
    8.10  (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
    8.11  fun mk_pointfree ctxt thm = thm
     9.1 --- a/src/HOL/Bali/Example.thy	Fri Dec 13 23:53:02 2013 +0100
     9.2 +++ b/src/HOL/Bali/Example.thy	Sat Dec 14 17:28:05 2013 +0100
     9.3 @@ -894,7 +894,7 @@
     9.4  
     9.5  declare member_is_static_simp [simp]
     9.6  declare wt.Skip [rule del] wt.Init [rule del]
     9.7 -ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
     9.8 +ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
     9.9  lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    9.10  lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    9.11  
    9.12 @@ -1189,7 +1189,7 @@
    9.13  
    9.14  ML {* bind_thms ("eval_intros", map 
    9.15          (simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o 
    9.16 -         rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    9.17 +         rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    9.18  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
    9.19  
    9.20  axiomatization
    10.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Dec 13 23:53:02 2013 +0100
    10.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Dec 14 17:28:05 2013 +0100
    10.3 @@ -2920,7 +2920,7 @@
    10.4  struct
    10.5  
    10.6  fun tactic ctxt alternative T ps = 
    10.7 -  Object_Logic.full_atomize_tac
    10.8 +  Object_Logic.full_atomize_tac ctxt
    10.9    THEN' CSUBGOAL (fn (g, i) =>
   10.10      let
   10.11        val th = frpar_oracle (ctxt, alternative, T, ps, g)
    11.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Dec 13 23:53:02 2013 +0100
    11.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 14 17:28:05 2013 +0100
    11.3 @@ -62,7 +62,7 @@
    11.4  fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    11.5  
    11.6  
    11.7 -fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
    11.8 +fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
    11.9    let
   11.10      val thy = Proof_Context.theory_of ctxt
   11.11      (* Transform the term*)
    12.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Dec 13 23:53:02 2013 +0100
    12.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Dec 14 17:28:05 2013 +0100
    12.3 @@ -66,7 +66,7 @@
    12.4  
    12.5  
    12.6  fun linr_tac ctxt q =
    12.7 -    Object_Logic.atomize_prems_tac
    12.8 +    Object_Logic.atomize_prems_tac ctxt
    12.9          THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
   12.10          THEN' SUBGOAL (fn (g, i) =>
   12.11    let
    13.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Dec 13 23:53:02 2013 +0100
    13.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Dec 14 17:28:05 2013 +0100
    13.3 @@ -224,7 +224,7 @@
    13.4    (case dlo_instance ctxt p of
    13.5      NONE => no_tac
    13.6    | SOME instance =>
    13.7 -      Object_Logic.full_atomize_tac i THEN
    13.8 +      Object_Logic.full_atomize_tac ctxt i THEN
    13.9        simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
   13.10        CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
   13.11        simp_tac ctxt i));  (* FIXME really? *)
    14.1 --- a/src/HOL/Decision_Procs/langford.ML	Fri Dec 13 23:53:02 2013 +0100
    14.2 +++ b/src/HOL/Decision_Procs/langford.ML	Sat Dec 14 17:28:05 2013 +0100
    14.3 @@ -237,11 +237,11 @@
    14.4    (case dlo_instance ctxt p of
    14.5      (ss, NONE) => simp_tac (put_simpset ss ctxt) i
    14.6    | (ss, SOME instance) =>
    14.7 -      Object_Logic.full_atomize_tac i THEN
    14.8 +      Object_Logic.full_atomize_tac ctxt i THEN
    14.9        simp_tac (put_simpset ss ctxt) i
   14.10        THEN (CONVERSION Thm.eta_long_conversion) i
   14.11        THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
   14.12 -      THEN Object_Logic.full_atomize_tac i
   14.13 +      THEN Object_Logic.full_atomize_tac ctxt i
   14.14        THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
   14.15        THEN (simp_tac (put_simpset ss ctxt) i)));
   14.16  end;
   14.17 \ No newline at end of file
    15.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Dec 13 23:53:02 2013 +0100
    15.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 14 17:28:05 2013 +0100
    15.3 @@ -82,7 +82,7 @@
    15.4  
    15.5  
    15.6  fun mir_tac ctxt q = 
    15.7 -    Object_Logic.atomize_prems_tac
    15.8 +    Object_Logic.atomize_prems_tac ctxt
    15.9          THEN' simp_tac (put_simpset HOL_basic_ss ctxt
   15.10            addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
   15.11          THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
    16.1 --- a/src/HOL/HOL.thy	Fri Dec 13 23:53:02 2013 +0100
    16.2 +++ b/src/HOL/HOL.thy	Sat Dec 14 17:28:05 2013 +0100
    16.3 @@ -1496,8 +1496,9 @@
    16.4                      | is_conj _ = false
    16.5                  in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
    16.6                | _ => NONE))]
    16.7 -    |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
    16.8 -      map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
    16.9 +    |> Simplifier.set_mksimps (fn ctxt =>
   16.10 +        Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
   16.11 +        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
   16.12  *}
   16.13  
   16.14  text {* Pre-simplification of induction and cases rules *}
    17.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Fri Dec 13 23:53:02 2013 +0100
    17.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Dec 14 17:28:05 2013 +0100
    17.3 @@ -208,29 +208,29 @@
    17.4    txt {* 10 - 7 *}
    17.5    apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
    17.6    txt {* 6 *}
    17.7 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    17.8 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
    17.9                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   17.10  
   17.11    txt {* 6 - 5 *}
   17.12    apply (tactic "EVERY1 [tac2,tac2]")
   17.13  
   17.14    txt {* 4 *}
   17.15 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   17.16 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
   17.17                                  (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   17.18    apply (tactic "tac2 1")
   17.19  
   17.20    txt {* 3 *}
   17.21 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   17.22 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
   17.23      (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
   17.24  
   17.25    apply (tactic "tac2 1")
   17.26 -  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
   17.27 +  apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
   17.28      (@{thm Impl.hdr_sum_def})] *})
   17.29    apply arith
   17.30  
   17.31    txt {* 2 *}
   17.32    apply (tactic "tac2 1")
   17.33 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   17.34 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
   17.35                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   17.36    apply (intro strip)
   17.37    apply (erule conjE)+
   17.38 @@ -238,11 +238,12 @@
   17.39  
   17.40    txt {* 1 *}
   17.41    apply (tactic "tac2 1")
   17.42 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   17.43 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
   17.44                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   17.45    apply (intro strip)
   17.46    apply (erule conjE)+
   17.47 -  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   17.48 +  apply (tactic {* fold_goals_tac @{context}
   17.49 +    [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   17.50    apply simp
   17.51  
   17.52    done
   17.53 @@ -286,13 +287,13 @@
   17.54    apply (intro strip, (erule conjE)+)
   17.55    apply (rule imp_disjL [THEN iffD1])
   17.56    apply (rule impI)
   17.57 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   17.58 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
   17.59      (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   17.60    apply simp
   17.61    apply (erule conjE)+
   17.62    apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
   17.63      k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
   17.64 -  apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
   17.65 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm inv1_def}]
   17.66                                  (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   17.67    apply (simp add: hdr_sum_def Multiset.count_def)
   17.68    apply (rule add_le_mono)
   17.69 @@ -307,7 +308,7 @@
   17.70    apply (intro strip, (erule conjE)+)
   17.71    apply (rule imp_disjL [THEN iffD1])
   17.72    apply (rule impI)
   17.73 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   17.74 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
   17.75      (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   17.76    apply simp
   17.77    done
   17.78 @@ -333,7 +334,7 @@
   17.79    txt {* 2 b *}
   17.80  
   17.81    apply (intro strip, (erule conjE)+)
   17.82 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   17.83 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
   17.84                                 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   17.85    apply simp
   17.86  
   17.87 @@ -341,9 +342,9 @@
   17.88    apply (tactic "tac4 1")
   17.89    apply (intro strip, (erule conjE)+)
   17.90    apply (rule ccontr)
   17.91 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   17.92 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
   17.93                                 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   17.94 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
   17.95 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
   17.96                                 (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
   17.97    apply simp
   17.98    apply (erule_tac x = "m" in allE)
    18.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Fri Dec 13 23:53:02 2013 +0100
    18.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sat Dec 14 17:28:05 2013 +0100
    18.3 @@ -101,8 +101,8 @@
    18.4      : thm =
    18.5    let
    18.6      fun tac {prems, context} =
    18.7 -      rewrite_goals_tac defs THEN
    18.8 -      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
    18.9 +      rewrite_goals_tac context defs THEN
   18.10 +      EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
   18.11    in
   18.12      Goal.prove_global thy [] [] goal tac
   18.13    end
   18.14 @@ -213,8 +213,10 @@
   18.15            in (n2, mk_ssumT (t1, t2)) end
   18.16        val ct = ctyp_of thy (snd (cons2typ 1 spec'))
   18.17        val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
   18.18 -      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
   18.19 -      val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2
   18.20 +      val thm2 = rewrite_rule (Proof_Context.init_global thy)
   18.21 +        (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
   18.22 +      val thm3 = rewrite_rule (Proof_Context.init_global thy)
   18.23 +        [mk_meta_eq @{thm conj_assoc}] thm2
   18.24  
   18.25        val y = Free ("y", lhsT)
   18.26        fun one_con (con, args) =
   18.27 @@ -225,15 +227,15 @@
   18.28          in Library.foldr mk_ex (vs, conj) end
   18.29        val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
   18.30        (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
   18.31 -      val tacs = [
   18.32 +      fun tacs {context = ctxt, prems} = [
   18.33            rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
   18.34 -          rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
   18.35 +          rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
   18.36            rtac thm3 1]
   18.37      in
   18.38 -      val nchotomy = prove thy con_betas goal (K tacs)
   18.39 +      val nchotomy = prove thy con_betas goal tacs
   18.40        val exhaust =
   18.41            (nchotomy RS @{thm exh_casedist0})
   18.42 -          |> rewrite_rule @{thms exh_casedists}
   18.43 +          |> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
   18.44            |> Drule.zero_var_indexes
   18.45      end
   18.46  
    19.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri Dec 13 23:53:02 2013 +0100
    19.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Dec 14 17:28:05 2013 +0100
    19.3 @@ -161,12 +161,12 @@
    19.4                val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules)
    19.5                fun arg_tac (lazy, _) =
    19.6                    rtac (if lazy then allI else case_UU_allI) 1
    19.7 -              val tacs =
    19.8 -                  rewrite_goals_tac @{thms atomize_all atomize_imp} ::
    19.9 +              fun tacs ctxt =
   19.10 +                  rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} ::
   19.11                    map arg_tac args @
   19.12                    [REPEAT (rtac impI 1), ALLGOALS simplify]
   19.13              in
   19.14 -              Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
   19.15 +              Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context)
   19.16              end
   19.17            fun eq_thms (p, cons) = map (con_thm p) cons
   19.18            val conss = map #con_specs constr_infos
   19.19 @@ -321,7 +321,7 @@
   19.20        val rules = @{thm Rep_cfun_strict1} :: take_0_thms
   19.21        fun tacf {prems, context = ctxt} =
   19.22          let
   19.23 -          val prem' = rewrite_rule [bisim_def_thm] (hd prems)
   19.24 +          val prem' = rewrite_rule ctxt [bisim_def_thm] (hd prems)
   19.25            val prems' = Project_Rule.projections ctxt prem'
   19.26            val dests = map (fn th => th RS spec RS spec RS mp) prems'
   19.27            fun one_tac (dest, rews) =
    20.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Dec 13 23:53:02 2013 +0100
    20.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Dec 14 17:28:05 2013 +0100
    20.3 @@ -157,10 +157,10 @@
    20.4      (* prove applied version of definitions *)
    20.5      fun prove_proj (lhs, rhs) =
    20.6        let
    20.7 -        val tac = rewrite_goals_tac fixdef_thms THEN
    20.8 +        fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
    20.9            (simp_tac (Simplifier.global_context thy beta_ss)) 1
   20.10          val goal = Logic.mk_equals (lhs, rhs)
   20.11 -      in Goal.prove_global thy [] [] goal (K tac) end
   20.12 +      in Goal.prove_global thy [] [] goal (tac o #context) end
   20.13      val proj_thms = map prove_proj projs
   20.14  
   20.15      (* mk_tuple lhss == fixpoint *)
   20.16 @@ -328,7 +328,7 @@
   20.17        in
   20.18          Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
   20.19           EVERY
   20.20 -          [rewrite_goals_tac map_apply_thms,
   20.21 +          [rewrite_goals_tac ctxt map_apply_thms,
   20.22             rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
   20.23             REPEAT (resolve_tac adm_rules 1),
   20.24             simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
   20.25 @@ -533,11 +533,11 @@
   20.26        let
   20.27          val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
   20.28          val DEFL_simps = RepData.get (Proof_Context.init_global thy)
   20.29 -        val tac =
   20.30 -          rewrite_goals_tac (map mk_meta_eq DEFL_simps)
   20.31 +        fun tac ctxt =
   20.32 +          rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
   20.33            THEN TRY (resolve_tac defl_unfold_thms 1)
   20.34        in
   20.35 -        Goal.prove_global thy [] [] goal (K tac)
   20.36 +        Goal.prove_global thy [] [] goal (tac o #context)
   20.37        end
   20.38      val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns
   20.39  
   20.40 @@ -641,7 +641,7 @@
   20.41        in
   20.42          Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
   20.43           EVERY
   20.44 -          [rewrite_goals_tac (defl_apply_thms @ map_apply_thms),
   20.45 +          [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
   20.46             rtac (@{thm cont_parallel_fix_ind}
   20.47               OF [defl_cont_thm, map_cont_thm]) 1,
   20.48             REPEAT (resolve_tac adm_rules 1),
    21.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Dec 13 23:53:02 2013 +0100
    21.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Dec 14 17:28:05 2013 +0100
    21.3 @@ -470,15 +470,15 @@
    21.4      fun prove_finite_thm (absT, finite_const) =
    21.5        let
    21.6          val goal = mk_trp (finite_const $ Free ("x", absT))
    21.7 -        val tac =
    21.8 +        fun tac ctxt =
    21.9              EVERY [
   21.10 -            rewrite_goals_tac finite_defs,
   21.11 +            rewrite_goals_tac ctxt finite_defs,
   21.12              rtac @{thm lub_ID_finite} 1,
   21.13              resolve_tac chain_take_thms 1,
   21.14              resolve_tac lub_take_thms 1,
   21.15              resolve_tac decisive_thms 1]
   21.16        in
   21.17 -        Goal.prove_global thy [] [] goal (K tac)
   21.18 +        Goal.prove_global thy [] [] goal (tac o #context)
   21.19        end
   21.20      val finite_thms =
   21.21          map prove_finite_thm (absTs ~~ finite_consts)
    22.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 13 23:53:02 2013 +0100
    22.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Dec 14 17:28:05 2013 +0100
    22.3 @@ -411,8 +411,8 @@
    22.4      : thm =
    22.5    let
    22.6      fun tac {prems, context} =
    22.7 -      rewrite_goals_tac defs THEN
    22.8 -      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
    22.9 +      rewrite_goals_tac context defs THEN
   22.10 +      EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
   22.11    in
   22.12      Goal.prove_global thy [] [] goal tac
   22.13    end;
    23.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Dec 13 23:53:02 2013 +0100
    23.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Dec 14 17:28:05 2013 +0100
    23.3 @@ -938,7 +938,7 @@
    23.4  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
    23.5  
    23.6  fun sos_tac print_cert prover ctxt =
    23.7 -  Object_Logic.full_atomize_tac THEN'
    23.8 +  Object_Logic.full_atomize_tac ctxt THEN'
    23.9    elim_denom_tac ctxt THEN'
   23.10    core_sos_tac print_cert prover ctxt;
   23.11  
    24.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Dec 13 23:53:02 2013 +0100
    24.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Dec 14 17:28:05 2013 +0100
    24.3 @@ -325,7 +325,7 @@
    24.4    apply(  fast intro: hext_trans)
    24.5  
    24.6  
    24.7 -apply( tactic prune_params_tac)
    24.8 +apply( tactic "prune_params_tac @{context}")
    24.9  -- "Level 52"
   24.10  
   24.11  -- "1 Call"
    25.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Dec 13 23:53:02 2013 +0100
    25.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat Dec 14 17:28:05 2013 +0100
    25.3 @@ -399,7 +399,7 @@
    25.4  
    25.5   fun norm_arith_tac ctxt =
    25.6     clarify_tac (put_claset HOL_cs ctxt) THEN'
    25.7 -   Object_Logic.full_atomize_tac THEN'
    25.8 +   Object_Logic.full_atomize_tac ctxt THEN'
    25.9     CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
   25.10  
   25.11  end;
    26.1 --- a/src/HOL/NSA/transfer.ML	Fri Dec 13 23:53:02 2013 +0100
    26.2 +++ b/src/HOL/NSA/transfer.ML	Sat Dec 14 17:28:05 2013 +0100
    26.3 @@ -58,11 +58,11 @@
    26.4      val meta = Local_Defs.meta_rewrite_rule ctxt;
    26.5      val ths' = map meta ths;
    26.6      val unfolds' = map meta unfolds and refolds' = map meta refolds;
    26.7 -    val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t))
    26.8 +    val (_$_$t') = concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (cterm_of thy t))
    26.9      val u = unstar_term consts t'
   26.10      val tac =
   26.11 -      rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
   26.12 -      ALLGOALS Object_Logic.full_atomize_tac THEN
   26.13 +      rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
   26.14 +      ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
   26.15        match_tac [transitive_thm] 1 THEN
   26.16        resolve_tac [@{thm transfer_start}] 1 THEN
   26.17        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
   26.18 @@ -76,7 +76,7 @@
   26.19                val tr = transfer_thm_of ctxt ths t
   26.20                val (_$l$r) = concl_of tr;
   26.21                val trs = if l aconv r then [] else [tr];
   26.22 -            in rewrite_goals_tac trs th end))
   26.23 +            in rewrite_goals_tac ctxt trs th end))
   26.24  
   26.25  local
   26.26  
    27.1 --- a/src/HOL/Nat.thy	Fri Dec 13 23:53:02 2013 +0100
    27.2 +++ b/src/HOL/Nat.thy	Sat Dec 14 17:28:05 2013 +0100
    27.3 @@ -1536,19 +1536,19 @@
    27.4  
    27.5  simproc_setup nateq_cancel_sums
    27.6    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    27.7 -  {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
    27.8 +  {* fn phi => try o Nat_Arith.cancel_eq_conv *}
    27.9  
   27.10  simproc_setup natless_cancel_sums
   27.11    ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
   27.12 -  {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
   27.13 +  {* fn phi => try o Nat_Arith.cancel_less_conv *}
   27.14  
   27.15  simproc_setup natle_cancel_sums
   27.16    ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
   27.17 -  {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
   27.18 +  {* fn phi => try o Nat_Arith.cancel_le_conv *}
   27.19  
   27.20  simproc_setup natdiff_cancel_sums
   27.21    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   27.22 -  {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
   27.23 +  {* fn phi => try o Nat_Arith.cancel_diff_conv *}
   27.24  
   27.25  ML_file "Tools/lin_arith.ML"
   27.26  setup {* Lin_Arith.global_setup *}
    28.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Dec 13 23:53:02 2013 +0100
    28.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Dec 14 17:28:05 2013 +0100
    28.3 @@ -829,6 +829,7 @@
    28.4         (* instantiations.                                                 *)
    28.5         val (_, thy33) =
    28.6           let
    28.7 +             val ctxt32 = Proof_Context.init_global thy32;
    28.8  
    28.9               (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
   28.10               (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
   28.11 @@ -918,7 +919,7 @@
   28.12              ||>> add_thmss_string
   28.13                let
   28.14                  val thms1 = inst_pt_at [all_eqvt];
   28.15 -                val thms2 = map (fold_rule [inductive_forall_def]) thms1
   28.16 +                val thms2 = map (fold_rule ctxt32 [inductive_forall_def]) thms1
   28.17                in
   28.18                  [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
   28.19                end
    29.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 13 23:53:02 2013 +0100
    29.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 14 17:28:05 2013 +0100
    29.3 @@ -134,7 +134,7 @@
    29.4  val at_fin_set_fresh = @{thm at_fin_set_fresh};
    29.5  val abs_fun_eq1 = @{thm abs_fun_eq1};
    29.6  
    29.7 -val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    29.8 +fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
    29.9  
   29.10  fun mk_perm Ts t u =
   29.11    let
   29.12 @@ -595,10 +595,12 @@
   29.13          end))
   29.14          (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
   29.15  
   29.16 +    val ctxt6 = Proof_Context.init_global thy6;
   29.17 +
   29.18      val perm_defs = map snd typedefs;
   29.19 -    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
   29.20 +    val Abs_inverse_thms = map (collect_simp ctxt6 o #Abs_inverse o snd o fst) typedefs;
   29.21      val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
   29.22 -    val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
   29.23 +    val Rep_thms = map (collect_simp ctxt6 o #Rep o snd o fst) typedefs;
   29.24  
   29.25  
   29.26      (** prove that new types are in class pt_<name> **)
   29.27 @@ -616,7 +618,7 @@
   29.28              (Sign.intern_type thy name,
   29.29                map (inter_sort thy sort o snd) tvs, [pt_class])
   29.30              (fn ctxt => EVERY [Class.intro_classes_tac [],
   29.31 -              rewrite_goals_tac [perm_def],
   29.32 +              rewrite_goals_tac ctxt [perm_def],
   29.33                asm_full_simp_tac (ctxt addsimps [Rep_inverse]) 1,
   29.34                asm_full_simp_tac (ctxt addsimps
   29.35                  [Rep RS perm_closed RS Abs_inverse]) 1,
   29.36 @@ -645,7 +647,7 @@
   29.37              (Sign.intern_type thy name,
   29.38                map (inter_sort thy sort o snd) tvs, [cp_class])
   29.39              (fn ctxt => EVERY [Class.intro_classes_tac [],
   29.40 -              rewrite_goals_tac [perm_def],
   29.41 +              rewrite_goals_tac ctxt [perm_def],
   29.42                asm_full_simp_tac (ctxt addsimps
   29.43                  ((Rep RS perm_closed1 RS Abs_inverse) ::
   29.44                   (if atom1 = atom2 then []
   29.45 @@ -783,7 +785,7 @@
   29.46          new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
   29.47        (thy7, [], [], []);
   29.48  
   29.49 -    val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
   29.50 +    val abs_inject_thms = map (collect_simp ctxt6 o #Abs_inject o snd o fst) typedefs
   29.51      val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
   29.52  
   29.53      (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
   29.54 @@ -792,9 +794,9 @@
   29.55        let
   29.56          val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
   29.57          val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
   29.58 -      in Goal.prove_global_future thy8 [] [] eqn (fn _ => EVERY
   29.59 +      in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY
   29.60          [resolve_tac inj_thms 1,
   29.61 -         rewrite_goals_tac rewrites,
   29.62 +         rewrite_goals_tac ctxt rewrites,
   29.63           rtac refl 3,
   29.64           resolve_tac rep_intrs 2,
   29.65           REPEAT (resolve_tac Rep_thms 1)])
   29.66 @@ -1043,7 +1045,7 @@
   29.67        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   29.68        (fn {prems, context = ctxt} => EVERY
   29.69          [rtac indrule_lemma' 1,
   29.70 -         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   29.71 +         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
   29.72           EVERY (map (fn (prem, r) => (EVERY
   29.73             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
   29.74              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
   29.75 @@ -2017,8 +2019,8 @@
   29.76          Goal.prove_global_future thy12 []
   29.77            (map (augment_sort thy12 fs_cp_sort) prems')
   29.78            (augment_sort thy12 fs_cp_sort concl')
   29.79 -          (fn {prems, ...} => EVERY
   29.80 -            [rewrite_goals_tac reccomb_defs,
   29.81 +          (fn {context = ctxt, prems} => EVERY
   29.82 +            [rewrite_goals_tac ctxt reccomb_defs,
   29.83               rtac @{thm the1_equality} 1,
   29.84               solve rec_unique_thms prems 1,
   29.85               resolve_tac rec_intrs 1,
    30.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Dec 13 23:53:02 2013 +0100
    30.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Dec 14 17:28:05 2013 +0100
    30.3 @@ -87,7 +87,7 @@
    30.4      val cert = Thm.cterm_of thy;
    30.5  
    30.6      val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
    30.7 -    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
    30.8 +    val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
    30.9  
   30.10      val finish_rule =
   30.11        split_all_tuples defs_ctxt
   30.12 @@ -101,7 +101,7 @@
   30.13      (fn i => fn st =>
   30.14        rules
   30.15        |> inst_mutual_rule ctxt insts avoiding
   30.16 -      |> Rule_Cases.consume (flat defs) facts
   30.17 +      |> Rule_Cases.consume ctxt (flat defs) facts
   30.18        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   30.19          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   30.20            (CONJUNCTS (ALLGOALS
   30.21 @@ -118,10 +118,10 @@
   30.22                   else
   30.23                     Induct.arbitrary_tac defs_ctxt k xs)
   30.24              end)
   30.25 -          THEN' Induct.inner_atomize_tac) j))
   30.26 -        THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
   30.27 +          THEN' Induct.inner_atomize_tac defs_ctxt) j))
   30.28 +        THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' =>
   30.29              Induct.guess_instance ctxt
   30.30 -              (finish_rule (Induct.internalize more_consumes rule)) i st'
   30.31 +              (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
   30.32              |> Seq.maps (fn rule' =>
   30.33                CASES (rule_cases ctxt rule' cases)
   30.34                  (rtac (rename_params_rule false [] rule') i THEN
   30.35 @@ -129,7 +129,7 @@
   30.36      THEN_ALL_NEW_CASES
   30.37        ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
   30.38          else K all_tac)
   30.39 -       THEN_ALL_NEW Induct.rulify_tac)
   30.40 +       THEN_ALL_NEW Induct.rulify_tac ctxt)
   30.41    end;
   30.42  
   30.43  
    31.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 13 23:53:02 2013 +0100
    31.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 14 17:28:05 2013 +0100
    31.3 @@ -373,8 +373,8 @@
    31.4            |> snd
    31.5          end)
    31.6        [goals] |>
    31.7 -    Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
    31.8 -      rewrite_goals_tac defs_thms THEN
    31.9 +    Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
   31.10 +      rewrite_goals_tac ctxt defs_thms THEN
   31.11        compose_tac (false, rule, length rule_prems) 1))) |>
   31.12      Seq.hd
   31.13    end;
    32.1 --- a/src/HOL/TLA/Action.thy	Fri Dec 13 23:53:02 2013 +0100
    32.2 +++ b/src/HOL/TLA/Action.thy	Sat Dec 14 17:28:05 2013 +0100
    32.3 @@ -108,23 +108,26 @@
    32.4     "world" parameter of the form (s,t) and apply additional rewrites.
    32.5  *)
    32.6  
    32.7 -fun action_unlift th =
    32.8 -  (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))
    32.9 -    handle THM _ => int_unlift th;
   32.10 +fun action_unlift ctxt th =
   32.11 +  (rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
   32.12 +    handle THM _ => int_unlift ctxt th;
   32.13  
   32.14  (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
   32.15  val action_rewrite = int_rewrite
   32.16  
   32.17 -fun action_use th =
   32.18 +fun action_use ctxt th =
   32.19      case (concl_of th) of
   32.20        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   32.21 -              (flatten (action_unlift th) handle THM _ => th)
   32.22 +              (flatten (action_unlift ctxt th) handle THM _ => th)
   32.23      | _ => th;
   32.24  *}
   32.25  
   32.26 -attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
   32.27 -attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
   32.28 -attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
   32.29 +attribute_setup action_unlift =
   32.30 +  {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
   32.31 +attribute_setup action_rewrite =
   32.32 +  {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
   32.33 +attribute_setup action_use =
   32.34 +  {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
   32.35  
   32.36  
   32.37  (* =========================== square / angle brackets =========================== *)
   32.38 @@ -258,11 +261,11 @@
   32.39     should plug in only "very safe" rules that can be applied blindly.
   32.40     Note that it applies whatever simplifications are currently active.
   32.41  *)
   32.42 -fun action_simp_tac ss intros elims =
   32.43 +fun action_simp_tac ctxt intros elims =
   32.44      asm_full_simp_tac
   32.45 -         (ss setloop (fn _ => (resolve_tac ((map action_use intros)
   32.46 +         (ctxt setloop (fn _ => (resolve_tac ((map (action_use ctxt) intros)
   32.47                                      @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
   32.48 -                      ORELSE' (eresolve_tac ((map action_use elims)
   32.49 +                      ORELSE' (eresolve_tac ((map (action_use ctxt) elims)
   32.50                                               @ [conjE,disjE,exE]))));
   32.51  *}
   32.52  
    33.1 --- a/src/HOL/TLA/Intensional.thy	Fri Dec 13 23:53:02 2013 +0100
    33.2 +++ b/src/HOL/TLA/Intensional.thy	Sat Dec 14 17:28:05 2013 +0100
    33.3 @@ -243,12 +243,12 @@
    33.4     |- F --> G  becomes   F w --> G w
    33.5  *)
    33.6  
    33.7 -fun int_unlift th =
    33.8 -  rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
    33.9 +fun int_unlift ctxt th =
   33.10 +  rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
   33.11  
   33.12  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
   33.13 -fun int_rewrite th =
   33.14 -  zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
   33.15 +fun int_rewrite ctxt th =
   33.16 +  zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
   33.17  
   33.18  (* flattening turns "-->" into "==>" and eliminates conjunctions in the
   33.19     antecedent. For example,
   33.20 @@ -282,17 +282,20 @@
   33.21      hflatten t
   33.22    end
   33.23  
   33.24 -fun int_use th =
   33.25 +fun int_use ctxt th =
   33.26      case (concl_of th) of
   33.27        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   33.28 -              (flatten (int_unlift th) handle THM _ => th)
   33.29 +              (flatten (int_unlift ctxt th) handle THM _ => th)
   33.30      | _ => th
   33.31  *}
   33.32  
   33.33 -attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
   33.34 -attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
   33.35 +attribute_setup int_unlift =
   33.36 +  {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
   33.37 +attribute_setup int_rewrite =
   33.38 +  {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
   33.39  attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
   33.40 -attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
   33.41 +attribute_setup int_use =
   33.42 +  {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
   33.43  
   33.44  lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   33.45    by (simp add: Valid_def)
    34.1 --- a/src/HOL/TLA/Memory/Memory.thy	Fri Dec 13 23:53:02 2013 +0100
    34.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Sat Dec 14 17:28:05 2013 +0100
    34.3 @@ -223,11 +223,11 @@
    34.4    apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
    34.5    apply (case_tac "arg (ch w p)")
    34.6     apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Read_def},
    34.7 -     temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
    34.8 +     temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
    34.9     apply (force dest: base_pair [temp_use])
   34.10    apply (erule contrapos_np)
   34.11    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Write_def},
   34.12 -    temp_rewrite @{thm enabled_ex}])
   34.13 +    temp_rewrite @{context} @{thm enabled_ex}])
   34.14      [@{thm WriteInner_enabled}, exI] [] 1 *})
   34.15    done
   34.16  
    35.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Dec 13 23:53:02 2013 +0100
    35.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Dec 14 17:28:05 2013 +0100
    35.3 @@ -233,7 +233,7 @@
    35.4  
    35.5  setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
    35.6  
    35.7 -ML {* val temp_elim = make_elim o temp_use *}
    35.8 +ML {* val temp_elim = make_elim oo temp_use *}
    35.9  
   35.10  
   35.11  
   35.12 @@ -352,7 +352,7 @@
   35.13           --> unchanged (rmhist!p)"
   35.14    by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
   35.15      @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
   35.16 -    @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
   35.17 +    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
   35.18  
   35.19  
   35.20  (* ------------------------------ State S2 ---------------------------------------- *)
   35.21 @@ -566,7 +566,8 @@
   35.22           & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
   35.23           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
   35.24    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   35.25 -      (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
   35.26 +      (map (temp_elim @{context})
   35.27 +        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
   35.28     using [[fast_solver]]
   35.29     apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
   35.30    done
   35.31 @@ -576,7 +577,8 @@
   35.32           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
   35.33               & unchanged (e p, r p, m p, rmhist!p)"
   35.34    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   35.35 -    (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
   35.36 +    (map (temp_elim @{context})
   35.37 +      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
   35.38     using [[fast_solver]]
   35.39     apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
   35.40    done
   35.41 @@ -586,9 +588,10 @@
   35.42           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
   35.43               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   35.44    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   35.45 -    (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   35.46 +    (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   35.47    apply (tactic {* action_simp_tac @{context} []
   35.48 -    (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
   35.49 +    (@{thm squareE} ::
   35.50 +      map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
   35.51     apply (auto dest!: S3Hist [temp_use])
   35.52    done
   35.53  
   35.54 @@ -599,9 +602,10 @@
   35.55               | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
   35.56               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   35.57    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   35.58 -    (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   35.59 +    (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   35.60    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
   35.61 -    (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
   35.62 +    (@{thm squareE} ::
   35.63 +      map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
   35.64    apply (auto dest!: S4Hist [temp_use])
   35.65    done
   35.66  
   35.67 @@ -610,8 +614,8 @@
   35.68           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
   35.69               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   35.70    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   35.71 -    (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
   35.72 -  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
   35.73 +    (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
   35.74 +  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
   35.75     using [[fast_solver]]
   35.76     apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
   35.77    done
   35.78 @@ -621,9 +625,9 @@
   35.79           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
   35.80               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   35.81    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   35.82 -    (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   35.83 +    (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   35.84    apply (tactic {* action_simp_tac @{context} []
   35.85 -    (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
   35.86 +    (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
   35.87       apply (auto dest: S6Hist [temp_use])
   35.88    done
   35.89  
   35.90 @@ -795,8 +799,8 @@
   35.91    SELECT_GOAL
   35.92     (TRY (rtac @{thm actionI} 1) THEN
   35.93      Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
   35.94 -    rewrite_goals_tac @{thms action_rews} THEN
   35.95 -    forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
   35.96 +    rewrite_goals_tac ctxt @{thms action_rews} THEN
   35.97 +    forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
   35.98      asm_full_simp_tac ctxt 1);
   35.99  *}
  35.100  
  35.101 @@ -898,7 +902,7 @@
  35.102  lemma S1_RNextdisabled: "|- S1 rmhist p -->
  35.103           ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
  35.104    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
  35.105 -    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
  35.106 +    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
  35.107    apply force
  35.108    done
  35.109  
  35.110 @@ -1103,7 +1107,7 @@
  35.111     apply (erule InfiniteEnsures)
  35.112      apply assumption
  35.113     apply (tactic {* action_simp_tac @{context} []
  35.114 -     (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
  35.115 +     (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
  35.116    apply (auto simp: SF_def)
  35.117    apply (erule contrapos_np)
  35.118    apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
  35.119 @@ -1190,7 +1194,7 @@
  35.120        ==> sigma |= []<>S1 rmhist p"
  35.121    apply (rule classical)
  35.122    apply (tactic {* asm_lr_simp_tac (@{context} addsimps
  35.123 -    [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
  35.124 +    [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
  35.125    apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
  35.126    done
  35.127  
    36.1 --- a/src/HOL/TLA/TLA.thy	Fri Dec 13 23:53:02 2013 +0100
    36.2 +++ b/src/HOL/TLA/TLA.thy	Sat Dec 14 17:28:05 2013 +0100
    36.3 @@ -118,25 +118,30 @@
    36.4     functions defined in theory Intensional in that they introduce a
    36.5     "world" parameter of type "behavior".
    36.6  *)
    36.7 -fun temp_unlift th =
    36.8 -  (rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th;
    36.9 +fun temp_unlift ctxt th =
   36.10 +  (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
   36.11 +    handle THM _ => action_unlift ctxt th;
   36.12  
   36.13  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
   36.14  val temp_rewrite = int_rewrite
   36.15  
   36.16 -fun temp_use th =
   36.17 +fun temp_use ctxt th =
   36.18    case (concl_of th) of
   36.19      Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
   36.20 -            ((flatten (temp_unlift th)) handle THM _ => th)
   36.21 +            ((flatten (temp_unlift ctxt th)) handle THM _ => th)
   36.22    | _ => th;
   36.23  
   36.24 -fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
   36.25 +fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
   36.26  *}
   36.27  
   36.28 -attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *}
   36.29 -attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *}
   36.30 -attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *}
   36.31 -attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
   36.32 +attribute_setup temp_unlift =
   36.33 +  {* Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of)) *}
   36.34 +attribute_setup temp_rewrite =
   36.35 +  {* Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of)) *}
   36.36 +attribute_setup temp_use =
   36.37 +  {* Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of)) *}
   36.38 +attribute_setup try_rewrite =
   36.39 +  {* Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of)) *}
   36.40  
   36.41  
   36.42  (* ------------------------------------------------------------------------- *)
   36.43 @@ -584,7 +589,7 @@
   36.44      (EVERY
   36.45       [auto_tac ctxt,
   36.46        TRY (merge_box_tac 1),
   36.47 -      rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
   36.48 +      rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *)
   36.49        TRYALL (etac @{thm Stable})]);
   36.50  
   36.51  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
    37.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Dec 13 23:53:02 2013 +0100
    37.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sat Dec 14 17:28:05 2013 +0100
    37.3 @@ -40,7 +40,7 @@
    37.4    in
    37.5      thms
    37.6      |> Conjunction.intr_balanced
    37.7 -    |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
    37.8 +    |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
    37.9      |> Thm.implies_intr assum
   37.10      |> Thm.generalize ([], params) 0
   37.11      |> Axclass.unoverload thy
   37.12 @@ -94,14 +94,14 @@
   37.13          (def, lthy')
   37.14        end;
   37.15  
   37.16 -    fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
   37.17 +    fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
   37.18  
   37.19      val qualify =
   37.20        Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
   37.21    in
   37.22      Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
   37.23      #> add_def
   37.24 -    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
   37.25 +    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
   37.26      #-> fold Code.del_eqn
   37.27      #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
   37.28      #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
    38.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 13 23:53:02 2013 +0100
    38.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 14 17:28:05 2013 +0100
    38.3 @@ -32,8 +32,6 @@
    38.4  val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
    38.5  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    38.6  
    38.7 -val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    38.8 -
    38.9  fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
   38.10    #exhaust (the (Symtab.lookup dt_info tname));
   38.11  
   38.12 @@ -271,6 +269,8 @@
   38.13  
   38.14      val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
   38.15  
   38.16 +    val collect_simp = rewrite_rule (Proof_Context.init_global thy4) [mk_meta_eq mem_Collect_eq];
   38.17 +
   38.18      val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) =>
   38.19        (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep));
   38.20  
   38.21 @@ -355,7 +355,7 @@
   38.22          val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
   38.23          val char_thms' =
   38.24            map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
   38.25 -            (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
   38.26 +            (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac refl 1])) eqns;
   38.27  
   38.28        in (thy', char_thms' @ char_thms) end;
   38.29  
   38.30 @@ -418,13 +418,13 @@
   38.31            Goal.prove_sorry_global thy5 [] []
   38.32              (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
   38.33              (fn {context = ctxt, ...} => EVERY
   38.34 -              [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   38.35 +              [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
   38.36                 REPEAT (EVERY
   38.37                   [rtac allI 1, rtac impI 1,
   38.38                    Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
   38.39                    REPEAT (EVERY
   38.40                      [hyp_subst_tac ctxt 1,
   38.41 -                     rewrite_goals_tac rewrites,
   38.42 +                     rewrite_goals_tac ctxt rewrites,
   38.43                       REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   38.44                       (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
   38.45                       ORELSE (EVERY
   38.46 @@ -443,9 +443,10 @@
   38.47          val elem_thm =
   38.48            Goal.prove_sorry_global thy5 [] []
   38.49              (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
   38.50 -            (fn _ =>
   38.51 -              EVERY [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   38.52 -                rewrite_goals_tac rewrites,
   38.53 +            (fn {context = ctxt, ...} =>
   38.54 +              EVERY [
   38.55 +                (Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
   38.56 +                rewrite_goals_tac ctxt rewrites,
   38.57                  REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
   38.58                    ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   38.59  
   38.60 @@ -480,11 +481,11 @@
   38.61        else
   38.62          drop (length newTs) (Datatype_Aux.split_conj_thm
   38.63            (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
   38.64 -             [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   38.65 +             [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
   38.66                REPEAT (rtac TrueI 1),
   38.67 -              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
   38.68 +              rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} ::
   38.69                  Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
   38.70 -              rewrite_goals_tac (map Thm.symmetric range_eqs),
   38.71 +              rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
   38.72                REPEAT (EVERY
   38.73                  [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   38.74                     maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
   38.75 @@ -511,9 +512,9 @@
   38.76          val rewrites = @{thm o_def} :: constr_defs @ map (mk_meta_eq o #2) newT_iso_axms;
   38.77        in
   38.78          Goal.prove_sorry_global thy5 [] [] eqn
   38.79 -        (fn _ => EVERY
   38.80 +        (fn {context = ctxt, ...} => EVERY
   38.81            [resolve_tac inj_thms 1,
   38.82 -           rewrite_goals_tac rewrites,
   38.83 +           rewrite_goals_tac ctxt rewrites,
   38.84             rtac refl 3,
   38.85             resolve_tac rep_intrs 2,
   38.86             REPEAT (resolve_tac iso_elem_thms 1)])
   38.87 @@ -634,7 +635,7 @@
   38.88        (fn {context = ctxt, prems, ...} =>
   38.89          EVERY
   38.90            [rtac indrule_lemma' 1,
   38.91 -           (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   38.92 +           (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
   38.93             EVERY (map (fn (prem, r) => (EVERY
   38.94               [REPEAT (eresolve_tac Abs_inverse_thms 1),
   38.95                simp_tac (put_simpset HOL_basic_ss ctxt
    39.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Dec 13 23:53:02 2013 +0100
    39.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Dec 14 17:28:05 2013 +0100
    39.3 @@ -27,6 +27,9 @@
    39.4  
    39.5  fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
    39.6    let
    39.7 +    val ctxt = Proof_Context.init_global thy;
    39.8 +    val cert = cterm_of thy;
    39.9 +
   39.10      val recTs = Datatype_Aux.get_rec_types descr;
   39.11      val pnames =
   39.12        if length descr = 1 then ["P"]
   39.13 @@ -104,7 +107,6 @@
   39.14          (map (fn ((((i, _), T), U), tname) =>
   39.15            make_pred i U T (mk_proj i is r) (Free (tname, T)))
   39.16              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   39.17 -    val cert = cterm_of thy;
   39.18      val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
   39.19        (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
   39.20  
   39.21 @@ -112,10 +114,10 @@
   39.22        Goal.prove_internal (map cert prems) (cert concl)
   39.23          (fn prems =>
   39.24             EVERY [
   39.25 -            rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
   39.26 +            rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
   39.27              rtac (cterm_instantiate inst induct) 1,
   39.28 -            ALLGOALS Object_Logic.atomize_prems_tac,
   39.29 -            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   39.30 +            ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
   39.31 +            rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   39.32              REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
   39.33                REPEAT (etac allE i) THEN atac i)) 1)])
   39.34        |> Drule.export_without_context;
    40.1 --- a/src/HOL/Tools/Datatype/primrec.ML	Fri Dec 13 23:53:02 2013 +0100
    40.2 +++ b/src/HOL/Tools/Datatype/primrec.ML	Sat Dec 14 17:28:05 2013 +0100
    40.3 @@ -245,8 +245,10 @@
    40.4        let
    40.5          val frees = fold (Variable.add_free_names ctxt) eqs [];
    40.6          val rewrites = rec_rewrites' @ map (snd o snd) defs;
    40.7 -        fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
    40.8 -      in map (fn eq => Goal.prove ctxt frees [] eq tac) eqs end;
    40.9 +      in
   40.10 +        map (fn eq => Goal.prove ctxt frees [] eq
   40.11 +          (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
   40.12 +      end;
   40.13    in ((prefix, (fs, defs)), prove) end
   40.14    handle PrimrecError (msg, some_eqn) =>
   40.15      error ("Primrec definition error:\n" ^ msg ^
    41.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Dec 13 23:53:02 2013 +0100
    41.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 14 17:28:05 2013 +0100
    41.3 @@ -207,8 +207,8 @@
    41.4            (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts))
    41.5            (fn {context = ctxt, ...} =>
    41.6              #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
    41.7 -              (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
    41.8 -                  rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
    41.9 +              (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
   41.10 +                  rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
   41.11        end;
   41.12  
   41.13      val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
   41.14 @@ -247,8 +247,8 @@
   41.15      val rec_thms =
   41.16        map (fn t =>
   41.17          Goal.prove_sorry_global thy2 [] [] t
   41.18 -          (fn _ => EVERY
   41.19 -            [rewrite_goals_tac reccomb_defs,
   41.20 +          (fn {context = ctxt, ...} => EVERY
   41.21 +            [rewrite_goals_tac ctxt reccomb_defs,
   41.22               rtac @{thm the1_equality} 1,
   41.23               resolve_tac rec_unique_thms 1,
   41.24               resolve_tac rec_intrs 1,
   41.25 @@ -327,8 +327,8 @@
   41.26      val case_thms =
   41.27        (map o map) (fn t =>
   41.28            Goal.prove_sorry_global thy2 [] [] t
   41.29 -            (fn _ =>
   41.30 -              EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
   41.31 +            (fn {context = ctxt, ...} =>
   41.32 +              EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
   41.33          (Datatype_Prop.make_cases case_names descr thy2);
   41.34    in
   41.35      thy2
    42.1 --- a/src/HOL/Tools/Function/function_lib.ML	Fri Dec 13 23:53:02 2013 +0100
    42.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Sat Dec 14 17:28:05 2013 +0100
    42.3 @@ -107,12 +107,14 @@
    42.4  
    42.5  fun regroup_conv neu cn ac is ct =
    42.6   let
    42.7 +   val thy = theory_of_cterm ct
    42.8 +   val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    42.9 +
   42.10     val mk = HOLogic.mk_binop cn
   42.11     val t = term_of ct
   42.12     val xs = dest_binop_list cn t
   42.13     val js = subtract (op =) is (0 upto (length xs) - 1)
   42.14     val ty = fastype_of t
   42.15 -   val thy = theory_of_cterm ct
   42.16   in
   42.17     Goal.prove_internal []
   42.18       (cterm_of thy
   42.19 @@ -122,7 +124,7 @@
   42.20            else if null js
   42.21              then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
   42.22              else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
   42.23 -     (K (rewrite_goals_tac ac
   42.24 +     (K (rewrite_goals_tac ctxt ac
   42.25           THEN rtac Drule.reflexive_thm 1))
   42.26   end
   42.27  
    43.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 13 23:53:02 2013 +0100
    43.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Dec 14 17:28:05 2013 +0100
    43.3 @@ -38,12 +38,12 @@
    43.4    branches: scheme_branch list,
    43.5    cases: scheme_case list}
    43.6  
    43.7 -val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
    43.8 -val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
    43.9 +fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize}
   43.10 +fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify}
   43.11  
   43.12  fun meta thm = thm RS eq_reflection
   43.13  
   43.14 -val sum_prod_conv = Raw_Simplifier.rewrite true
   43.15 +fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
   43.16    (map meta (@{thm split_conv} :: @{thms sum.cases}))
   43.17  
   43.18  fun term_conv thy cv t =
   43.19 @@ -187,13 +187,15 @@
   43.20    end
   43.21  
   43.22  
   43.23 -fun mk_ind_goal thy branches =
   43.24 +fun mk_ind_goal ctxt branches =
   43.25    let
   43.26 +    val thy = Proof_Context.theory_of ctxt
   43.27 +
   43.28      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   43.29        HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   43.30        |> fold_rev (curry Logic.mk_implies) Cs
   43.31        |> fold_rev (Logic.all o Free) ws
   43.32 -      |> term_conv thy ind_atomize
   43.33 +      |> term_conv thy (ind_atomize ctxt)
   43.34        |> Object_Logic.drop_judgment thy
   43.35        |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   43.36    in
   43.37 @@ -203,6 +205,9 @@
   43.38  fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
   43.39    (IndScheme {T, cases=scases, branches}) =
   43.40    let
   43.41 +    val thy = Proof_Context.theory_of ctxt
   43.42 +    val cert = cterm_of thy
   43.43 +
   43.44      val n = length branches
   43.45      val scases_idx = map_index I scases
   43.46  
   43.47 @@ -210,10 +215,7 @@
   43.48        SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
   43.49      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
   43.50  
   43.51 -    val thy = Proof_Context.theory_of ctxt
   43.52 -    val cert = cterm_of thy
   43.53 -
   43.54 -    val P_comp = mk_ind_goal thy branches
   43.55 +    val P_comp = mk_ind_goal ctxt branches
   43.56  
   43.57      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   43.58      val ihyp = Logic.all_const T $ Abs ("z", T,
   43.59 @@ -270,8 +272,8 @@
   43.60                  sih
   43.61                  |> Thm.forall_elim (cert (inject idx rcargs))
   43.62                  |> Thm.elim_implies (import ineq) (* Psum rcargs *)
   43.63 -                |> Conv.fconv_rule sum_prod_conv
   43.64 -                |> Conv.fconv_rule ind_rulify
   43.65 +                |> Conv.fconv_rule (sum_prod_conv ctxt)
   43.66 +                |> Conv.fconv_rule (ind_rulify ctxt)
   43.67                  |> (fn th => th COMP ipres) (* P rs *)
   43.68                  |> fold_rev (Thm.implies_intr o cprop_of) cGas
   43.69                  |> fold_rev Thm.forall_intr cGvs
   43.70 @@ -312,8 +314,9 @@
   43.71  
   43.72          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   43.73            |> Goal.init
   43.74 -          |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   43.75 -              THEN CONVERSION ind_rulify 1)
   43.76 +          |> (Simplifier.rewrite_goals_tac ctxt
   43.77 +                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   43.78 +              THEN CONVERSION (ind_rulify ctxt) 1)
   43.79            |> Seq.hd
   43.80            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   43.81            |> Goal.finish ctxt
   43.82 @@ -375,7 +378,7 @@
   43.83          indthm
   43.84          |> Drule.instantiate' [] [SOME inst]
   43.85          |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
   43.86 -        |> Conv.fconv_rule ind_rulify
   43.87 +        |> Conv.fconv_rule (ind_rulify ctxt'')
   43.88        end
   43.89  
   43.90      val res = Conjunction.intr_balanced (map_index project branches)
    44.1 --- a/src/HOL/Tools/Function/partial_function.ML	Fri Dec 13 23:53:02 2013 +0100
    44.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sat Dec 14 17:28:05 2013 +0100
    44.3 @@ -180,6 +180,7 @@
    44.4      val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
    44.5      val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
    44.6    in 
    44.7 +    (* FIXME ctxt vs. ctxt' (!?) *)
    44.8      rule
    44.9      |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
   44.10      |> Tactic.rule_by_tactic ctxt
   44.11 @@ -188,7 +189,7 @@
   44.12         THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
   44.13      |> (fn thm => thm OF [mono_thm, f_def])
   44.14      |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
   44.15 -         (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}])) 
   44.16 +         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
   44.17      |> singleton (Variable.export ctxt' ctxt)
   44.18    end
   44.19  
    45.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Dec 13 23:53:02 2013 +0100
    45.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Dec 14 17:28:05 2013 +0100
    45.3 @@ -305,7 +305,7 @@
    45.4    in
    45.5      (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
    45.6       THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
    45.7 -     THEN rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
    45.8 +     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
    45.9    end
   45.10  
   45.11  end
    46.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Dec 13 23:53:02 2013 +0100
    46.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sat Dec 14 17:28:05 2013 +0100
    46.3 @@ -85,7 +85,7 @@
    46.4        in
    46.5          Conv.fconv_rule 
    46.6            ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
    46.7 -            (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
    46.8 +            (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
    46.9        end
   46.10  
   46.11      fun inst_relcomppI thy ant1 ant2 =
   46.12 @@ -482,7 +482,7 @@
   46.13      val eq_thm = 
   46.14        (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   46.15    in
   46.16 -    Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
   46.17 +    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   46.18    end
   46.19  
   46.20  fun rename_to_tnames ctxt term =
   46.21 @@ -533,7 +533,8 @@
   46.22            fun after_qed' thm_list lthy = 
   46.23              let
   46.24                val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm 
   46.25 -                  (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
   46.26 +                  (fn {context = ctxt, ...} =>
   46.27 +                    rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
   46.28              in
   46.29                after_qed internal_rsp_thm lthy
   46.30              end
    47.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Dec 13 23:53:02 2013 +0100
    47.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Dec 14 17:28:05 2013 +0100
    47.3 @@ -552,9 +552,9 @@
    47.4     @{const_name Let}]
    47.5  
    47.6  fun presimplify ctxt =
    47.7 -  rewrite_rule (map safe_mk_meta_eq nnf_simps)
    47.8 +  rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps)
    47.9    #> simplify (put_simpset nnf_ss ctxt)
   47.10 -  #> rewrite_rule @{thms Let_def [abs_def]}
   47.11 +  #> rewrite_rule ctxt @{thms Let_def [abs_def]}
   47.12  
   47.13  fun make_nnf ctxt th = case prems_of th of
   47.14      [] => th |> presimplify ctxt |> make_nnf1 ctxt
   47.15 @@ -706,7 +706,7 @@
   47.16    Function mkcl converts theorems to clauses.*)
   47.17  fun MESON preskolem_tac mkcl cltac ctxt i st =
   47.18    SELECT_GOAL
   47.19 -    (EVERY [Object_Logic.atomize_prems_tac 1,
   47.20 +    (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
   47.21              rtac ccontr 1,
   47.22              preskolem_tac,
   47.23              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
    48.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 13 23:53:02 2013 +0100
    48.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Dec 14 17:28:05 2013 +0100
    48.3 @@ -193,6 +193,8 @@
    48.4     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
    48.5  fun old_skolem_theorem_of_def thy rhs0 =
    48.6    let
    48.7 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    48.8 +
    48.9      val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
   48.10      val rhs' = rhs |> Thm.dest_comb |> snd
   48.11      val (ch, frees) = c_variant_abs_multi (rhs', [])
   48.12 @@ -208,8 +210,8 @@
   48.13        Drule.list_comb (rhs, frees)
   48.14        |> Drule.beta_conv cabs |> Thm.apply cTrueprop
   48.15      fun tacf [prem] =
   48.16 -      rewrite_goals_tac @{thms skolem_def [abs_def]}
   48.17 -      THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
   48.18 +      rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
   48.19 +      THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
   48.20                   RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
   48.21    in
   48.22      Goal.prove_internal [ex_tm] conc tacf
   48.23 @@ -308,7 +310,7 @@
   48.24           |> zero_var_indexes
   48.25           |> new_skolem ? forall_intr_vars
   48.26      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
   48.27 -    val th = th |> Conv.fconv_rule Object_Logic.atomize
   48.28 +    val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
   48.29                  |> cong_extensionalize_thm thy
   48.30                  |> abs_extensionalize_thm ctxt
   48.31                  |> make_nnf ctxt
    49.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Fri Dec 13 23:53:02 2013 +0100
    49.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Sat Dec 14 17:28:05 2013 +0100
    49.3 @@ -135,8 +135,8 @@
    49.4    Isa_Raw of thm
    49.5  
    49.6  val proxy_defs = map (fst o snd o snd) proxy_table
    49.7 -val prepare_helper =
    49.8 -  Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
    49.9 +fun prepare_helper ctxt =
   49.10 +  Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
   49.11  
   49.12  fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
   49.13    if is_tptp_variable s then
   49.14 @@ -160,7 +160,7 @@
   49.15  fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
   49.16      maps (metis_literals_of_atp type_enc) phis
   49.17    | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
   49.18 -fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
   49.19 +fun metis_axiom_of_atp ctxt type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
   49.20      let
   49.21        fun some isa =
   49.22          SOME (phi |> metis_literals_of_atp type_enc
   49.23 @@ -178,7 +178,7 @@
   49.24            nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
   49.25                 |> the)
   49.26                (the (Int.fromString j) - 1)
   49.27 -          |> snd |> prepare_helper
   49.28 +          |> snd |> prepare_helper ctxt
   49.29            |> Isa_Raw |> some
   49.30          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
   49.31        else case try (unprefix fact_prefix) ident of
   49.32 @@ -196,7 +196,7 @@
   49.33          end
   49.34        | NONE => TrueI |> Isa_Raw |> some
   49.35      end
   49.36 -  | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
   49.37 +  | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
   49.38  
   49.39  fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
   49.40      eliminate_lam_wrappers t
   49.41 @@ -249,7 +249,7 @@
   49.42      (* "rev" is for compatibility with existing proof scripts. *)
   49.43      val axioms =
   49.44        atp_problem
   49.45 -      |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
   49.46 +      |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
   49.47      fun ord_info () = atp_problem_term_order_info atp_problem
   49.48    in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
   49.49  
    50.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Dec 13 23:53:02 2013 +0100
    50.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Dec 14 17:28:05 2013 +0100
    50.3 @@ -249,16 +249,16 @@
    50.4     "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
    50.5     don't use this trick in general because it makes the proof object uglier than
    50.6     necessary. FIXME. *)
    50.7 -fun negate_head th =
    50.8 +fun negate_head ctxt th =
    50.9    if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
   50.10      (th RS @{thm select_FalseI})
   50.11 -    |> fold (rewrite_rule o single)
   50.12 +    |> fold (rewrite_rule ctxt o single)
   50.13              @{thms not_atomize_select atomize_not_select}
   50.14    else
   50.15 -    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
   50.16 +    th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
   50.17  
   50.18  (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   50.19 -val select_literal = negate_head oo make_last
   50.20 +fun select_literal ctxt = negate_head ctxt oo make_last
   50.21  
   50.22  fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
   50.23    let
   50.24 @@ -293,7 +293,7 @@
   50.25                i_th2)
   50.26             | j2 =>
   50.27               (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
   50.28 -              resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
   50.29 +              resolve_inc_tyvars thy (select_literal ctxt j1 i_th1) j2 i_th2
   50.30                handle TERM (s, _) =>
   50.31                       raise METIS_RECONSTRUCT ("resolve_inference", s)))
   50.32        end
   50.33 @@ -448,7 +448,7 @@
   50.34                             |> distinct Term.aconv_untyped
   50.35          val goal = Logic.list_implies (prems, concl)
   50.36          val tac = cut_tac th 1
   50.37 -                  THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
   50.38 +                  THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]}
   50.39                    THEN ALLGOALS assume_tac
   50.40        in
   50.41          if length prems = length prems0 then
    51.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Dec 13 23:53:02 2013 +0100
    51.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Dec 14 17:28:05 2013 +0100
    51.3 @@ -65,7 +65,7 @@
    51.4  fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
    51.5    let
    51.6      val thy = Proof_Context.theory_of ctxt
    51.7 -    val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
    51.8 +    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
    51.9      val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
   51.10      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   51.11    in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
    52.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 13 23:53:02 2013 +0100
    52.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Dec 14 17:28:05 2013 +0100
    52.3 @@ -219,8 +219,8 @@
    52.4            |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
    52.5          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
    52.6          val case_th =
    52.7 -          rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
    52.8 -        val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
    52.9 +          rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
   52.10 +        val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
   52.11          val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
   52.12          val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
   52.13            OF (replicate nargs @{thm refl})
   52.14 @@ -236,7 +236,7 @@
   52.15        (PEEK nprems_of
   52.16          (fn n =>
   52.17            ALLGOALS (fn i =>
   52.18 -            rewrite_goal_tac [@{thm split_paired_all}] i
   52.19 +            rewrite_goal_tac ctxt [@{thm split_paired_all}] i
   52.20              THEN (SUBPROOF (instantiate i n) ctxt i))))
   52.21    in
   52.22      Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
    53.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 13 23:53:02 2013 +0100
    53.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Dec 14 17:28:05 2013 +0100
    53.3 @@ -1017,8 +1017,9 @@
    53.4  
    53.5  fun peephole_optimisation thy intro =
    53.6    let
    53.7 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    53.8      val process =
    53.9 -      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
   53.10 +      rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
   53.11      fun process_False intro_t =
   53.12        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
   53.13      fun process_True intro_t =
    54.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 13 23:53:02 2013 +0100
    54.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Dec 14 17:28:05 2013 +0100
    54.3 @@ -203,7 +203,7 @@
    54.4      SOME specss => (specss, thy)
    54.5    | NONE =>*)
    54.6      let
    54.7 -      val ctxt = Proof_Context.init_global thy
    54.8 +      val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
    54.9        val intros =
   54.10          if forall is_pred_equation specs then 
   54.11            map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
   54.12 @@ -213,7 +213,7 @@
   54.13            error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   54.14              ^ commas (map (quote o Display.string_of_thm_global thy) specs))
   54.15        val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
   54.16 -      val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
   54.17 +      val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
   54.18        val _ = print_specs options thy "normalized intros" intros
   54.19        (*val intros = maps (split_cases thy) intros*)
   54.20        val (intros', (local_defs, thy')) = flatten_intros constname intros thy
    55.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 13 23:53:02 2013 +0100
    55.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Dec 14 17:28:05 2013 +0100
    55.3 @@ -79,11 +79,11 @@
    55.4           @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
    55.5           @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
    55.6      | Free _ =>
    55.7 -      Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
    55.8 +      Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
    55.9          let
   55.10            val prems' = maps dest_conjunct_prem (take nargs prems)
   55.11          in
   55.12 -          rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   55.13 +          rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   55.14          end) ctxt 1
   55.15      | Abs _ => raise Fail "prove_param: No valid parameter term"
   55.16    in
   55.17 @@ -118,7 +118,7 @@
   55.18        end
   55.19    | (Free _, _) =>
   55.20      print_tac options "proving parameter call.."
   55.21 -    THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
   55.22 +    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
   55.23          let
   55.24            val param_prem = nth prems premposition
   55.25            val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
   55.26 @@ -126,7 +126,7 @@
   55.27            fun param_rewrite prem =
   55.28              param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
   55.29            val SOME rew_eq = find_first param_rewrite prems'
   55.30 -          val param_prem' = rewrite_rule
   55.31 +          val param_prem' = rewrite_rule ctxt'
   55.32              (map (fn th => th RS @{thm eq_reflection})
   55.33                [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   55.34              param_prem
   55.35 @@ -168,7 +168,7 @@
   55.36                  let
   55.37                    val prems' = maps dest_conjunct_prem (take nargs prems)
   55.38                  in
   55.39 -                  rewrite_goal_tac
   55.40 +                  rewrite_goal_tac ctxt
   55.41                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   55.42                  end
   55.43               THEN REPEAT_DETERM (rtac @{thm refl} 1))
   55.44 @@ -205,12 +205,12 @@
   55.45        THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
   55.46        THEN print_tac options "before single intro rule"
   55.47        THEN Subgoal.FOCUS_PREMS
   55.48 -             (fn {context, params, prems, asms, concl, schematics} =>
   55.49 -              let
   55.50 -                val prems' = maps dest_conjunct_prem (take nargs prems)
   55.51 -              in
   55.52 -                rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   55.53 -              end) ctxt 1
   55.54 +         (fn {context = ctxt', params, prems, asms, concl, schematics} =>
   55.55 +          let
   55.56 +            val prems' = maps dest_conjunct_prem (take nargs prems)
   55.57 +          in
   55.58 +            rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   55.59 +          end) ctxt 1
   55.60        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   55.61      | prove_prems out_ts ((p, deriv) :: ps) =
   55.62        let
   55.63 @@ -293,7 +293,7 @@
   55.64      val nargs = length (binder_types T)
   55.65      val pred_case_rule = the_elim_of ctxt pred
   55.66    in
   55.67 -    REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))
   55.68 +    REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
   55.69      THEN print_tac options "before applying elim rule"
   55.70      THEN etac (predfun_elim_of ctxt pred mode) 1
   55.71      THEN etac pred_case_rule 1
   55.72 @@ -370,7 +370,7 @@
   55.73            val ho_args = ho_args_of mode args
   55.74          in
   55.75            etac @{thm bindE} 1
   55.76 -          THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
   55.77 +          THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
   55.78            THEN print_tac options "prove_expr2-before"
   55.79            THEN etac (predfun_elim_of ctxt name mode) 1
   55.80            THEN print_tac options "prove_expr2"
   55.81 @@ -483,11 +483,11 @@
   55.82        THEN (prove_clause2 options ctxt pred mode clause i)
   55.83    in
   55.84      (DETERM (TRY (rtac @{thm unit.induct} 1)))
   55.85 -     THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
   55.86 +     THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
   55.87       THEN (rtac (predfun_intro_of ctxt pred mode) 1)
   55.88       THEN (REPEAT_DETERM (rtac @{thm refl} 2))
   55.89 -     THEN (if null moded_clauses then
   55.90 -         etac @{thm botE} 1
   55.91 +     THEN (
   55.92 +       if null moded_clauses then etac @{thm botE} 1
   55.93         else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
   55.94    end;
   55.95  
    56.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Dec 13 23:53:02 2013 +0100
    56.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 14 17:28:05 2013 +0100
    56.3 @@ -865,19 +865,19 @@
    56.4      val aprems = Arith_Data.get_arith_facts ctxt
    56.5    in
    56.6      Method.insert_tac aprems
    56.7 -    THEN_ALL_NEW Object_Logic.full_atomize_tac
    56.8 +    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    56.9      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   56.10      THEN_ALL_NEW simp_tac simpset_ctxt
   56.11      THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
   56.12 -    THEN_ALL_NEW Object_Logic.full_atomize_tac
   56.13 +    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
   56.14      THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
   56.15 -    THEN_ALL_NEW Object_Logic.full_atomize_tac
   56.16 +    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
   56.17      THEN_ALL_NEW div_mod_tac ctxt
   56.18      THEN_ALL_NEW splits_tac ctxt
   56.19      THEN_ALL_NEW simp_tac simpset_ctxt
   56.20      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   56.21      THEN_ALL_NEW nat_to_int_tac ctxt
   56.22 -    THEN_ALL_NEW (core_tac ctxt)
   56.23 +    THEN_ALL_NEW core_tac ctxt
   56.24      THEN_ALL_NEW finish_tac elim
   56.25    end 1);
   56.26  
    57.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 13 23:53:02 2013 +0100
    57.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Dec 14 17:28:05 2013 +0100
    57.3 @@ -107,7 +107,7 @@
    57.4      fun tac ctxt =
    57.5        ALLGOALS (rtac rule)
    57.6        THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
    57.7 -      THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
    57.8 +      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
    57.9      val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
   57.10    in (simp, lthy') end;
   57.11  
   57.12 @@ -166,7 +166,7 @@
   57.13      fun prove_simps proto_simps lthy =
   57.14        let
   57.15          val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
   57.16 -        val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
   57.17 +        val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
   57.18        in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
   57.19      val b = Binding.conceal (Binding.qualify true prfx
   57.20        (Binding.qualify true name (Binding.name "simps")));
    58.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 13 23:53:02 2013 +0100
    58.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Dec 14 17:28:05 2013 +0100
    58.3 @@ -129,7 +129,7 @@
    58.4      val eq_thm = 
    58.5        (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
    58.6    in
    58.7 -    Object_Logic.rulify (eq_thm RS Drule.equal_elim_rule2)
    58.8 +    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
    58.9    end
   58.10  
   58.11  
   58.12 @@ -187,7 +187,7 @@
   58.13            case thm_list of
   58.14              [] => the maybe_proven_rsp_thm
   58.15            | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm 
   58.16 -            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
   58.17 +            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
   58.18        in
   58.19          snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
   58.20        end
    59.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Dec 13 23:53:02 2013 +0100
    59.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Dec 14 17:28:05 2013 +0100
    59.3 @@ -40,10 +40,10 @@
    59.4  (* composition of two theorems, used in maps *)
    59.5  fun OF1 thm1 thm2 = thm2 RS thm1
    59.6  
    59.7 -fun atomize_thm thm =
    59.8 +fun atomize_thm ctxt thm =
    59.9    let
   59.10      val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
   59.11 -    val thm'' = Object_Logic.atomize (cprop_of thm')
   59.12 +    val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
   59.13    in
   59.14      @{thm equal_elim_rule1} OF [thm'', thm']
   59.15    end
   59.16 @@ -480,7 +480,7 @@
   59.17          val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
   59.18          val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   59.19          val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
   59.20 -        val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
   59.21 +        val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
   59.22          val (insp, inst) =
   59.23            if ty_c = ty_d
   59.24            then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   59.25 @@ -635,7 +635,7 @@
   59.26      val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
   59.27    in
   59.28      full_simp_tac simpset
   59.29 -    THEN' Object_Logic.full_atomize_tac
   59.30 +    THEN' Object_Logic.full_atomize_tac ctxt
   59.31      THEN' gen_frees_tac ctxt
   59.32      THEN' SUBGOAL (fn (goal, i) =>
   59.33        let
   59.34 @@ -652,7 +652,7 @@
   59.35      val mk_tac_raw =
   59.36        descend_procedure_tac ctxt simps
   59.37        THEN' RANGE
   59.38 -        [Object_Logic.rulify_tac THEN' (K all_tac),
   59.39 +        [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
   59.40           regularize_tac ctxt,
   59.41           all_injection_tac ctxt,
   59.42           clean_tac ctxt]
   59.43 @@ -685,7 +685,7 @@
   59.44      val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
   59.45    in
   59.46      full_simp_tac simpset
   59.47 -    THEN' Object_Logic.full_atomize_tac
   59.48 +    THEN' Object_Logic.full_atomize_tac ctxt
   59.49      THEN' gen_frees_tac ctxt
   59.50      THEN' SUBGOAL (fn (goal, i) =>
   59.51        let
   59.52 @@ -702,7 +702,7 @@
   59.53      val mk_tac_raw =
   59.54        partiality_descend_procedure_tac ctxt simps
   59.55        THEN' RANGE
   59.56 -        [Object_Logic.rulify_tac THEN' (K all_tac),
   59.57 +        [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
   59.58           all_injection_tac ctxt,
   59.59           clean_tac ctxt]
   59.60    in
   59.61 @@ -720,7 +720,7 @@
   59.62      val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
   59.63    in
   59.64      full_simp_tac simpset
   59.65 -    THEN' Object_Logic.full_atomize_tac
   59.66 +    THEN' Object_Logic.full_atomize_tac ctxt
   59.67      THEN' gen_frees_tac ctxt
   59.68      THEN' SUBGOAL (fn (goal, i) =>
   59.69        let
   59.70 @@ -730,7 +730,7 @@
   59.71            rthm |> full_simplify simpset
   59.72                 |> Drule.eta_contraction_rule
   59.73                 |> Thm.forall_intr_frees
   59.74 -               |> atomize_thm
   59.75 +               |> atomize_thm ctxt
   59.76  
   59.77          val rule = procedure_inst ctxt (prop_of rthm') goal
   59.78        in
    60.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Dec 13 23:53:02 2013 +0100
    60.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Sat Dec 14 17:28:05 2013 +0100
    60.3 @@ -193,7 +193,7 @@
    60.4      val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
    60.5      val quotient_thm =
    60.6        (quot_thm RS @{thm quot_type.Quotient})
    60.7 -      |> fold_rule [abs_def, rep_def]
    60.8 +      |> fold_rule lthy3 [abs_def, rep_def]
    60.9  
   60.10      (* name equivalence theorem *)
   60.11      val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
    61.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Fri Dec 13 23:53:02 2013 +0100
    61.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Sat Dec 14 17:28:05 2013 +0100
    61.3 @@ -68,7 +68,7 @@
    61.4  fun prove_inj_prop ctxt def lhs =
    61.5    let
    61.6      val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
    61.7 -    val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
    61.8 +    val rule = disjE OF [Object_Logic.rulify ctxt (Thm.assume lhs)]
    61.9    in
   61.10      Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
   61.11      |> apply (rtac @{thm injI})
   61.12 @@ -94,7 +94,7 @@
   61.13  
   61.14  fun prove_lhs ctxt rhs =
   61.15    let
   61.16 -    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
   61.17 +    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
   61.18      val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
   61.19    in
   61.20      Z3_Proof_Tools.by_tac (
    62.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Dec 13 23:53:02 2013 +0100
    62.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Dec 14 17:28:05 2013 +0100
    62.3 @@ -38,16 +38,19 @@
    62.4      val merge = Net.merge eq
    62.5    )
    62.6  
    62.7 -  val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
    62.8 +  fun prep context =
    62.9 +    `Thm.prop_of o rewrite_rule (Context.proof_of context) [Z3_Proof_Literals.rewrite_true]
   62.10  
   62.11 -  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
   62.12 -  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
   62.13 +  fun ins thm context =
   62.14 +    context |> Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
   62.15 +  fun rem thm context =
   62.16 +    context |> Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
   62.17  
   62.18 -  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
   62.19 -  val del = Thm.declaration_attribute (Z3_Rules.map o del)
   62.20 +  val add = Thm.declaration_attribute ins
   62.21 +  val del = Thm.declaration_attribute rem
   62.22  in
   62.23  
   62.24 -val add_z3_rule = Z3_Rules.map o ins
   62.25 +val add_z3_rule = ins
   62.26  
   62.27  fun by_schematic_rule ctxt ct =
   62.28    the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
    63.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Dec 13 23:53:02 2013 +0100
    63.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Dec 14 17:28:05 2013 +0100
    63.3 @@ -68,10 +68,11 @@
    63.4    |   _ => r RS P_imp_P_eq_True
    63.5  
    63.6  (*Is this the best way to invoke the simplifier??*)
    63.7 -fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
    63.8 +fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
    63.9  
   63.10  fun join_assums th =
   63.11    let val thy = Thm.theory_of_thm th
   63.12 +      val ctxt = Proof_Context.init_global thy
   63.13        val tych = cterm_of thy
   63.14        val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
   63.15        val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
   63.16 @@ -80,7 +81,7 @@
   63.17    in
   63.18      Rules.GEN_ALL
   63.19        (Rules.DISCH_ALL
   63.20 -         (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
   63.21 +         (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
   63.22    end
   63.23    val gen_all = USyntax.gen_all
   63.24  in
   63.25 @@ -139,7 +140,7 @@
   63.26     let
   63.27         val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
   63.28         val {rules,rows,TCs,full_pats_TCs} =
   63.29 -           Prim.post_definition congs (thy, (def, pats))
   63.30 +           Prim.post_definition congs thy ctxt (def, pats)
   63.31         val {lhs=f,rhs} = USyntax.dest_eq (concl def)
   63.32         val (_,[R,_]) = USyntax.strip_comb rhs
   63.33         val dummy = Prim.trace_thms "congs =" congs
   63.34 @@ -149,9 +150,9 @@
   63.35                 {f = f, R = R, rules = rules,
   63.36                  full_pats_TCs = full_pats_TCs,
   63.37                  TCs = TCs}
   63.38 -       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
   63.39 +       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
   63.40                          (Rules.CONJUNCTS rules)
   63.41 -         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
   63.42 +         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
   63.43          rules = ListPair.zip(rules', rows),
   63.44          tcs = (termination_goals rules') @ tcs}
   63.45     end
   63.46 @@ -170,7 +171,7 @@
   63.47      | solve_eq _ (th, [a], i) = [(a, i)]
   63.48      | solve_eq ctxt (th, splitths, i) =
   63.49        (writeln "Proving unsplit equation...";
   63.50 -      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
   63.51 +      [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
   63.52            (CaseSplit.splitto ctxt splitths th), i)])
   63.53        handle ERROR s => 
   63.54               (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
    64.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Dec 13 23:53:02 2013 +0100
    64.2 +++ b/src/HOL/Tools/TFL/rules.ML	Sat Dec 14 17:28:05 2013 +0100
    64.3 @@ -42,14 +42,14 @@
    64.4    val DISJ_CASESL: thm -> thm list -> thm
    64.5  
    64.6    val list_beta_conv: cterm -> cterm list -> thm
    64.7 -  val SUBS: thm list -> thm -> thm
    64.8 +  val SUBS: Proof.context -> thm list -> thm -> thm
    64.9    val simpl_conv: Proof.context -> thm list -> cterm -> thm
   64.10  
   64.11    val rbeta: thm -> thm
   64.12    val tracing: bool Unsynchronized.ref
   64.13    val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
   64.14                               -> thm -> thm * term list
   64.15 -  val RIGHT_ASSOC: thm -> thm
   64.16 +  val RIGHT_ASSOC: Proof.context -> thm -> thm
   64.17  
   64.18    val prove: bool -> cterm * tactic -> thm
   64.19  end;
   64.20 @@ -417,8 +417,8 @@
   64.21   *        Rewriting
   64.22   *---------------------------------------------------------------------------*)
   64.23  
   64.24 -fun SUBS thl =
   64.25 -  rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
   64.26 +fun SUBS ctxt thl =
   64.27 +  rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
   64.28  
   64.29  val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
   64.30  
   64.31 @@ -426,7 +426,7 @@
   64.32   rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
   64.33  
   64.34  
   64.35 -val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
   64.36 +fun RIGHT_ASSOC ctxt = rewrite_rule ctxt [Thms.disj_assoc];
   64.37  
   64.38  
   64.39  
   64.40 @@ -602,24 +602,24 @@
   64.41   *  the wrong word to use).
   64.42   *---------------------------------------------------------------------------*)
   64.43  
   64.44 -fun VSTRUCT_ELIM tych a vstr th =
   64.45 +fun VSTRUCT_ELIM ctxt tych a vstr th =
   64.46    let val L = USyntax.free_vars_lr vstr
   64.47        val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   64.48 -      val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
   64.49 +      val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
   64.50        val thm2 = forall_intr_list (map tych L) thm1
   64.51        val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   64.52    in refl RS
   64.53 -     rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
   64.54 +     rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
   64.55    end;
   64.56  
   64.57 -fun PGEN tych a vstr th =
   64.58 +fun PGEN ctxt tych a vstr th =
   64.59    let val a1 = tych a
   64.60        val vstr1 = tych vstr
   64.61    in
   64.62    Thm.forall_intr a1
   64.63       (if (is_Free vstr)
   64.64        then cterm_instantiate [(vstr1,a1)] th
   64.65 -      else VSTRUCT_ELIM tych a vstr th)
   64.66 +      else VSTRUCT_ELIM ctxt tych a vstr th)
   64.67    end;
   64.68  
   64.69  
   64.70 @@ -701,7 +701,7 @@
   64.71                    val impth = implies_intr_list ants1 QeeqQ3
   64.72                    val impth1 = impth RS meta_eq_to_obj_eq
   64.73                    (* Need to abstract *)
   64.74 -                  val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
   64.75 +                  val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
   64.76                in ant_th COMP thm
   64.77                end
   64.78               fun q_eliminate (thm,imp,thy) =
    65.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri Dec 13 23:53:02 2013 +0100
    65.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sat Dec 14 17:28:05 2013 +0100
    65.3 @@ -12,7 +12,7 @@
    65.4    type pattern
    65.5    val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    65.6    val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    65.7 -  val post_definition: thm list -> theory * (thm * pattern list) ->
    65.8 +  val post_definition: thm list -> theory -> Proof.context -> thm * pattern list ->
    65.9     {rules: thm,
   65.10      rows: int list,
   65.11      TCs: term list list,
   65.12 @@ -415,7 +415,7 @@
   65.13  
   65.14  fun givens pats = map pat_of (filter given pats);
   65.15  
   65.16 -fun post_definition meta_tflCongs (theory, (def, pats)) =
   65.17 +fun post_definition meta_tflCongs theory ctxt (def, pats) =
   65.18   let val tych = Thry.typecheck theory
   65.19       val f = #lhs(USyntax.dest_eq(concl def))
   65.20       val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
   65.21 @@ -440,7 +440,7 @@
   65.22       val extract = Rules.CONTEXT_REWRITE_RULE
   65.23                       (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
   65.24       val (rules, TCs) = ListPair.unzip (map extract corollaries')
   65.25 -     val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   65.26 +     val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
   65.27       val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   65.28       val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
   65.29   in
   65.30 @@ -460,7 +460,8 @@
   65.31   *---------------------------------------------------------------------------*)
   65.32  
   65.33  fun wfrec_eqns thy fid tflCongs eqns =
   65.34 - let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
   65.35 + let val ctxt = Proof_Context.init_global thy
   65.36 +     val {lhs,rhs} = USyntax.dest_eq (hd eqns)
   65.37       val (f,args) = USyntax.strip_comb lhs
   65.38       val (fname,fty) = dest_atom f
   65.39       val (SV,a) = front_last args    (* SV = schematic variables *)
   65.40 @@ -493,7 +494,7 @@
   65.41       val R1 = USyntax.rand WFR
   65.42       val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
   65.43       val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
   65.44 -     val corollaries' = map (rewrite_rule case_rewrites) corollaries
   65.45 +     val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries
   65.46       fun extract X = Rules.CONTEXT_REWRITE_RULE
   65.47                         (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
   65.48   in {proto_def = proto_def,
   65.49 @@ -625,6 +626,7 @@
   65.50  
   65.51  fun mk_case ty_info usednames thy =
   65.52   let
   65.53 + val ctxt = Proof_Context.init_global thy
   65.54   val divide = ipartition (gvvariant usednames)
   65.55   val tych = Thry.typecheck thy
   65.56   fun tych_binding(x,y) = (tych x, tych y)
   65.57 @@ -657,7 +659,7 @@
   65.58                                     (new_formals, disjuncts)
   65.59              val constraints = map #1 existentials
   65.60              val vexl = map #2 existentials
   65.61 -            fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
   65.62 +            fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
   65.63              val news = map (fn (nf,rows,c) => {path = nf@rstp,
   65.64                                                 rows = map (expnd c) rows})
   65.65                             (Utils.zip3 new_formals groups constraints)
   65.66 @@ -675,7 +677,8 @@
   65.67  
   65.68  
   65.69  fun complete_cases thy =
   65.70 - let val tych = Thry.typecheck thy
   65.71 + let val ctxt = Proof_Context.init_global thy
   65.72 +     val tych = Thry.typecheck thy
   65.73       val ty_info = Thry.induct_info thy
   65.74   in fn pats =>
   65.75   let val names = List.foldr Misc_Legacy.add_term_names [] pats
   65.76 @@ -691,7 +694,7 @@
   65.77       val rows = map (fn x => ([x], (th0,[]))) pats
   65.78   in
   65.79   Rules.GEN (tych a)
   65.80 -       (Rules.RIGHT_ASSOC
   65.81 +       (Rules.RIGHT_ASSOC ctxt
   65.82            (Rules.CHOOSE(tych v, ex_th0)
   65.83                  (mk_case ty_info (vname::aname::names)
   65.84                   thy {path=[v], rows=rows})))
   65.85 @@ -826,7 +829,8 @@
   65.86   * the antecedent of Rinduct.
   65.87   *---------------------------------------------------------------------------*)
   65.88  fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
   65.89 -let val tych = Thry.typecheck thy
   65.90 +let val ctxt = Proof_Context.init_global thy
   65.91 +    val tych = Thry.typecheck thy
   65.92      val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   65.93      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   65.94      val case_thm = complete_cases thy pats
   65.95 @@ -848,7 +852,7 @@
   65.96            domain)
   65.97      val vtyped = tych v
   65.98      val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   65.99 -    val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
  65.100 +    val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
  65.101                            (substs, proved_cases)
  65.102      val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
  65.103      val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
    66.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Dec 13 23:53:02 2013 +0100
    66.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Dec 14 17:28:05 2013 +0100
    66.3 @@ -113,6 +113,8 @@
    66.4  
    66.5  fun process_spec axiomatic cos alt_props thy =
    66.6      let
    66.7 +        val ctxt = Proof_Context.init_global thy
    66.8 +
    66.9          fun zip3 [] [] [] = []
   66.10            | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
   66.11            | zip3 _ _ _ = error "Choice_Specification.process_spec internal error"
   66.12 @@ -122,7 +124,7 @@
   66.13            | myfoldr f [] = error "Choice_Specification.process_spec internal error"
   66.14  
   66.15          val rew_imps = alt_props |>
   66.16 -          map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
   66.17 +          map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
   66.18          val props' = rew_imps |>
   66.19            map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
   66.20  
    67.1 --- a/src/HOL/Tools/coinduction.ML	Fri Dec 13 23:53:02 2013 +0100
    67.2 +++ b/src/HOL/Tools/coinduction.ML	Sat Dec 14 17:28:05 2013 +0100
    67.3 @@ -53,9 +53,9 @@
    67.4      val cases = Rule_Cases.get raw_thm |> fst
    67.5    in
    67.6      NO_CASES (HEADGOAL (
    67.7 -      Object_Logic.rulify_tac THEN'
    67.8 +      Object_Logic.rulify_tac ctxt THEN'
    67.9        Method.insert_tac prems THEN'
   67.10 -      Object_Logic.atomize_prems_tac THEN'
   67.11 +      Object_Logic.atomize_prems_tac ctxt THEN'
   67.12        DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
   67.13          let
   67.14            val vars = raw_vars @ map (term_of o snd) params;
   67.15 @@ -110,7 +110,7 @@
   67.16                          unfold_thms_tac ctxt eqs
   67.17                        end)) ctxt)))])
   67.18          end) ctxt) THEN'
   67.19 -      K (prune_params_tac))) st
   67.20 +      K (prune_params_tac ctxt))) st
   67.21      |> Seq.maps (fn (_, st) =>
   67.22        CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
   67.23    end;
    68.1 --- a/src/HOL/Tools/groebner.ML	Fri Dec 13 23:53:02 2013 +0100
    68.2 +++ b/src/HOL/Tools/groebner.ML	Sat Dec 14 17:28:05 2013 +0100
    68.3 @@ -928,7 +928,7 @@
    68.4      delsimps del_thms addsimps add_thms);
    68.5  
    68.6  fun ring_tac add_ths del_ths ctxt =
    68.7 -  Object_Logic.full_atomize_tac
    68.8 +  Object_Logic.full_atomize_tac ctxt
    68.9    THEN' presimplify ctxt add_ths del_ths
   68.10    THEN' CSUBGOAL (fn (p, i) =>
   68.11      rtac (let val form = Object_Logic.dest_judgment p
   68.12 @@ -970,7 +970,7 @@
   68.13     end
   68.14    in
   68.15       clarify_tac (put_claset claset ctxt) i
   68.16 -     THEN Object_Logic.full_atomize_tac i
   68.17 +     THEN Object_Logic.full_atomize_tac ctxt i
   68.18       THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
   68.19       THEN clarify_tac (put_claset claset ctxt) i
   68.20       THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
    69.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 13 23:53:02 2013 +0100
    69.2 +++ b/src/HOL/Tools/inductive.ML	Sat Dec 14 17:28:05 2013 +0100
    69.3 @@ -396,7 +396,7 @@
    69.4  
    69.5      val intrs = map_index (fn (i, intr) =>
    69.6        Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
    69.7 -       [rewrite_goals_tac rec_preds_defs,
    69.8 +       [rewrite_goals_tac ctxt rec_preds_defs,
    69.9          rtac (unfold RS iffD2) 1,
   69.10          EVERY1 (select_disj (length intr_ts) (i + 1)),
   69.11          (*Not ares_tac, since refl must be tried before any equality assumptions;
   69.12 @@ -440,14 +440,15 @@
   69.13             map mk_elim_prem (map #1 c_intrs)
   69.14        in
   69.15          (Goal.prove_sorry ctxt'' [] prems P
   69.16 -          (fn {prems, ...} => EVERY
   69.17 +          (fn {context = ctxt4, prems} => EVERY
   69.18              [cut_tac (hd prems) 1,
   69.19 -             rewrite_goals_tac rec_preds_defs,
   69.20 +             rewrite_goals_tac ctxt4 rec_preds_defs,
   69.21               dtac (unfold RS iffD1) 1,
   69.22               REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   69.23               REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   69.24               EVERY (map (fn prem =>
   69.25 -               DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
   69.26 +               DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
   69.27 +                (tl prems))])
   69.28            |> singleton (Proof_Context.export ctxt'' ctxt'''),
   69.29           map #2 c_intrs, length Ts)
   69.30        end
   69.31 @@ -503,12 +504,12 @@
   69.32            (if null ts andalso null us then rtac intr 1
   69.33             else
   69.34              EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
   69.35 -            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   69.36 +            Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
   69.37                let
   69.38                  val (eqs, prems') = chop (length us) prems;
   69.39                  val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
   69.40                in
   69.41 -                rewrite_goal_tac rew_thms 1 THEN
   69.42 +                rewrite_goal_tac ctxt'' rew_thms 1 THEN
   69.43                  rtac intr 1 THEN
   69.44                  EVERY (map (fn p => rtac p 1) prems')
   69.45                end) ctxt' 1);
   69.46 @@ -545,7 +546,7 @@
   69.47  
   69.48  in
   69.49  
   69.50 -fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
   69.51 +fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt;
   69.52  
   69.53  fun mk_cases ctxt prop =
   69.54    let
   69.55 @@ -598,7 +599,7 @@
   69.56            val props = Syntax.read_props ctxt' raw_props;
   69.57            val ctxt'' = fold Variable.declare_term props ctxt';
   69.58            val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
   69.59 -        in Method.erule 0 rules end))
   69.60 +        in Method.erule ctxt 0 rules end))
   69.61      "dynamic case analysis on predicates";
   69.62  
   69.63  
   69.64 @@ -724,30 +725,30 @@
   69.65      val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
   69.66  
   69.67      val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
   69.68 -      (fn {prems, ...} => EVERY
   69.69 -        [rewrite_goals_tac [inductive_conj_def],
   69.70 +      (fn {context = ctxt3, prems} => EVERY
   69.71 +        [rewrite_goals_tac ctxt3 [inductive_conj_def],
   69.72           DETERM (rtac raw_fp_induct 1),
   69.73           REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
   69.74 -         rewrite_goals_tac simp_thms2,
   69.75 +         rewrite_goals_tac ctxt3 simp_thms2,
   69.76           (*This disjE separates out the introduction rules*)
   69.77           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
   69.78           (*Now break down the individual cases.  No disjE here in case
   69.79             some premise involves disjunction.*)
   69.80 -         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
   69.81 +         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
   69.82           REPEAT (FIRSTGOAL
   69.83             (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
   69.84 -         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
   69.85 +         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
   69.86               (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
   69.87             conjI, refl] 1)) prems)]);
   69.88  
   69.89      val lemma = Goal.prove_sorry ctxt'' [] []
   69.90 -      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
   69.91 -        [rewrite_goals_tac rec_preds_defs,
   69.92 +      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
   69.93 +        [rewrite_goals_tac ctxt3 rec_preds_defs,
   69.94           REPEAT (EVERY
   69.95             [REPEAT (resolve_tac [conjI, impI] 1),
   69.96              REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
   69.97              atac 1,
   69.98 -            rewrite_goals_tac simp_thms1,
   69.99 +            rewrite_goals_tac ctxt3 simp_thms1,
  69.100              atac 1])]);
  69.101  
  69.102    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
  69.103 @@ -961,9 +962,9 @@
  69.104        (if no_ind then Drule.asm_rl
  69.105         else if coind then
  69.106           singleton (Proof_Context.export lthy2 lthy1)
  69.107 -           (rotate_prems ~1 (Object_Logic.rulify
  69.108 -             (fold_rule rec_preds_defs
  69.109 -               (rewrite_rule simp_thms3
  69.110 +           (rotate_prems ~1 (Object_Logic.rulify lthy2
  69.111 +             (fold_rule lthy2 rec_preds_defs
  69.112 +               (rewrite_rule lthy2 simp_thms3
  69.113                  (mono RS (fp_def RS @{thm def_coinduct}))))))
  69.114         else
  69.115           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
    70.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Dec 13 23:53:02 2013 +0100
    70.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Dec 14 17:28:05 2013 +0100
    70.3 @@ -393,11 +393,11 @@
    70.4          val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
    70.5          val thm = Goal.prove_global thy []
    70.6            (map attach_typeS prems) (attach_typeS concl)
    70.7 -          (fn {prems, ...} => EVERY
    70.8 +          (fn {context = ctxt, prems} => EVERY
    70.9            [rtac (#raw_induct ind_info) 1,
   70.10 -           rewrite_goals_tac rews,
   70.11 +           rewrite_goals_tac ctxt rews,
   70.12             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   70.13 -             [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
   70.14 +             [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
   70.15                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   70.16          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   70.17            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   70.18 @@ -459,8 +459,8 @@
   70.19              [cut_tac (hd prems) 1,
   70.20               etac elimR 1,
   70.21               ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
   70.22 -             rewrite_goals_tac rews,
   70.23 -             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
   70.24 +             rewrite_goals_tac ctxt rews,
   70.25 +             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
   70.26                 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   70.27          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   70.28            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
    71.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Dec 13 23:53:02 2013 +0100
    71.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Dec 14 17:28:05 2013 +0100
    71.3 @@ -871,8 +871,9 @@
    71.4  
    71.5  in
    71.6  
    71.7 -fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
    71.8 -  Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
    71.9 +fun gen_tac ex ctxt =
   71.10 +  FIRST' [simple_tac ctxt,
   71.11 +    Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
   71.12  
   71.13  val tac = gen_tac true;
   71.14  
    72.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Dec 13 23:53:02 2013 +0100
    72.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Dec 14 17:28:05 2013 +0100
    72.3 @@ -6,10 +6,10 @@
    72.4  
    72.5  signature NAT_ARITH =
    72.6  sig
    72.7 -  val cancel_diff_conv: conv
    72.8 -  val cancel_eq_conv: conv
    72.9 -  val cancel_le_conv: conv
   72.10 -  val cancel_less_conv: conv
   72.11 +  val cancel_diff_conv: Proof.context -> conv
   72.12 +  val cancel_eq_conv: Proof.context -> conv
   72.13 +  val cancel_le_conv: Proof.context -> conv
   72.14 +  val cancel_less_conv: Proof.context -> conv
   72.15  end;
   72.16  
   72.17  structure Nat_Arith: NAT_ARITH =
   72.18 @@ -26,9 +26,9 @@
   72.19  
   72.20  val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
   72.21  
   72.22 -fun move_to_front path = Conv.every_conv
   72.23 +fun move_to_front ctxt path = Conv.every_conv
   72.24      [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
   72.25 -     Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
   72.26 +     Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
   72.27  
   72.28  fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
   72.29        add_atoms (add1::path) x #> add_atoms (add2::path) y
   72.30 @@ -54,12 +54,12 @@
   72.31      find (sort ord' xs) (sort ord' ys)
   72.32    end
   72.33  
   72.34 -fun cancel_conv rule ct =
   72.35 +fun cancel_conv rule ctxt ct =
   72.36    let
   72.37      val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
   72.38      val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
   72.39 -    val lconv = move_to_front lpath
   72.40 -    val rconv = move_to_front rpath
   72.41 +    val lconv = move_to_front ctxt lpath
   72.42 +    val rconv = move_to_front ctxt rpath
   72.43      val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
   72.44      val conv = conv1 then_conv Conv.rewr_conv rule
   72.45    in conv ct end
    73.1 --- a/src/HOL/Tools/record.ML	Fri Dec 13 23:53:02 2013 +0100
    73.2 +++ b/src/HOL/Tools/record.ML	Sat Dec 14 17:28:05 2013 +0100
    73.3 @@ -1616,9 +1616,9 @@
    73.4  
    73.5      val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
    73.6        Goal.prove_sorry_global defs_thy [] [] split_meta_prop
    73.7 -        (fn _ =>
    73.8 +        (fn {context = ctxt, ...} =>
    73.9            EVERY1
   73.10 -           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
   73.11 +           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
   73.12              etac @{thm meta_allE}, atac,
   73.13              rtac (@{thm prop_subst} OF [surject]),
   73.14              REPEAT o etac @{thm meta_allE}, atac]));
   73.15 @@ -1742,12 +1742,13 @@
   73.16          HOLogic.mk_Trueprop (HOLogic.mk_eq
   73.17            (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
   73.18             Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
   73.19 -      fun tac eq_def =
   73.20 +      fun tac ctxt eq_def =
   73.21          Class.intro_classes_tac []
   73.22 -        THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
   73.23 +        THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
   73.24          THEN ALLGOALS (rtac @{thm refl});
   73.25        fun mk_eq thy eq_def =
   73.26 -        rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
   73.27 +        rewrite_rule (Proof_Context.init_global thy)
   73.28 +          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
   73.29        fun mk_eq_refl thy =
   73.30          @{thm equal_refl}
   73.31          |> Thm.instantiate
   73.32 @@ -1765,8 +1766,7 @@
   73.33        |-> (fn eq => Specification.definition
   73.34              (NONE, (Attrib.empty_binding, eq)))
   73.35        |-> (fn (_, (_, eq_def)) =>
   73.36 -         Class.prove_instantiation_exit_result Morphism.thm
   73.37 -            (fn _ => fn eq_def => tac eq_def) eq_def)
   73.38 +         Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
   73.39        |-> (fn eq_def => fn thy =>
   73.40              thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
   73.41        |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
   73.42 @@ -2139,18 +2139,18 @@
   73.43  
   73.44      val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
   73.45        Goal.prove_sorry_global defs_thy [] [] split_meta_prop
   73.46 -        (fn _ =>
   73.47 +        (fn {context = ctxt', ...} =>
   73.48            EVERY1
   73.49 -           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
   73.50 +           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
   73.51              etac @{thm meta_allE}, atac,
   73.52              rtac (@{thm prop_subst} OF [surjective]),
   73.53              REPEAT o etac @{thm meta_allE}, atac]));
   73.54  
   73.55      val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
   73.56        Goal.prove_sorry_global defs_thy [] [] split_object_prop
   73.57 -        (fn _ =>
   73.58 +        (fn {context = ctxt, ...} =>
   73.59            rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
   73.60 -          rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
   73.61 +          rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
   73.62            rtac split_meta 1));
   73.63  
   73.64      val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
    74.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri Dec 13 23:53:02 2013 +0100
    74.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat Dec 14 17:28:05 2013 +0100
    74.3 @@ -427,9 +427,9 @@
    74.4  (*      subgoal                                                              *)
    74.5  (* ------------------------------------------------------------------------- *)
    74.6  
    74.7 -val pre_cnf_tac =
    74.8 +fun pre_cnf_tac ctxt =
    74.9    rtac ccontr THEN'
   74.10 -  Object_Logic.atomize_prems_tac THEN'
   74.11 +  Object_Logic.atomize_prems_tac ctxt THEN'
   74.12    CONVERSION Drule.beta_eta_conversion;
   74.13  
   74.14  (* ------------------------------------------------------------------------- *)
   74.15 @@ -460,7 +460,7 @@
   74.16  (* ------------------------------------------------------------------------- *)
   74.17  
   74.18  fun sat_tac ctxt i =
   74.19 -  pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   74.20 +  pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   74.21  
   74.22  (* ------------------------------------------------------------------------- *)
   74.23  (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   74.24 @@ -469,6 +469,6 @@
   74.25  (* ------------------------------------------------------------------------- *)
   74.26  
   74.27  fun satx_tac ctxt i =
   74.28 -  pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   74.29 +  pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   74.30  
   74.31  end;
    75.1 --- a/src/HOL/Tools/simpdata.ML	Fri Dec 13 23:53:02 2013 +0100
    75.2 +++ b/src/HOL/Tools/simpdata.ML	Sat Dec 14 17:28:05 2013 +0100
    75.3 @@ -71,10 +71,10 @@
    75.4          Goal.prove_global (Thm.theory_of_thm st) []
    75.5            [mk_simp_implies @{prop "(x::'a) == y"}]
    75.6            (mk_simp_implies @{prop "(x::'a) = y"})
    75.7 -          (fn {prems, ...} => EVERY
    75.8 -           [rewrite_goals_tac @{thms simp_implies_def},
    75.9 +          (fn {context = ctxt, prems} => EVERY
   75.10 +           [rewrite_goals_tac ctxt @{thms simp_implies_def},
   75.11              REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
   75.12 -              map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
   75.13 +              map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
   75.14        end
   75.15    end;
   75.16  
    76.1 --- a/src/HOL/Tools/transfer.ML	Fri Dec 13 23:53:02 2013 +0100
    76.2 +++ b/src/HOL/Tools/transfer.ML	Sat Dec 14 17:28:05 2013 +0100
    76.3 @@ -193,7 +193,7 @@
    76.4      by (unfold is_equality_def, rule, drule meta_spec,
    76.5        erule meta_mp, rule refl, simp)}
    76.6  
    76.7 -fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
    76.8 +fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
    76.9    let
   76.10      val thy = Thm.theory_of_thm thm
   76.11      val prop = Thm.prop_of thm
   76.12 @@ -212,7 +212,7 @@
   76.13      val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
   76.14      val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
   76.15      val cprop = Thm.cterm_of thy prop2
   76.16 -    val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
   76.17 +    val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
   76.18      fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   76.19    in
   76.20      forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   76.21 @@ -234,11 +234,11 @@
   76.22        Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
   76.23        handle CTERM _ => thm
   76.24    in
   76.25 -    gen_abstract_equalities dest contracted_eq_thm
   76.26 +    gen_abstract_equalities ctxt dest contracted_eq_thm
   76.27    end
   76.28  
   76.29 -fun abstract_equalities_relator_eq rel_eq_thm =
   76.30 -  gen_abstract_equalities (fn x => (x, I))
   76.31 +fun abstract_equalities_relator_eq ctxt rel_eq_thm =
   76.32 +  gen_abstract_equalities ctxt (fn x => (x, I))
   76.33      (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
   76.34  
   76.35  fun abstract_equalities_domain ctxt thm =
   76.36 @@ -256,7 +256,7 @@
   76.37      val contracted_eq_thm = 
   76.38        Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
   76.39    in
   76.40 -    gen_abstract_equalities dest contracted_eq_thm
   76.41 +    gen_abstract_equalities ctxt dest contracted_eq_thm
   76.42    end 
   76.43  
   76.44  
   76.45 @@ -288,7 +288,7 @@
   76.46            | t => t)
   76.47    end
   76.48  
   76.49 -fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
   76.50 +fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
   76.51    let
   76.52      val thy = Thm.theory_of_thm thm
   76.53      val prop = Thm.prop_of thm
   76.54 @@ -305,14 +305,14 @@
   76.55      val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
   76.56      val prop2 = Logic.list_rename_params (rev names) prop1
   76.57      val cprop = Thm.cterm_of thy prop2
   76.58 -    val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
   76.59 +    val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
   76.60      fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   76.61    in
   76.62      forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   76.63    end
   76.64      handle TERM _ => thm
   76.65  
   76.66 -fun abstract_domains_transfer thm =
   76.67 +fun abstract_domains_transfer ctxt thm =
   76.68    let
   76.69      fun dest prop =
   76.70        let
   76.71 @@ -324,7 +324,7 @@
   76.72            Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
   76.73        end
   76.74    in
   76.75 -    gen_abstract_domains dest thm
   76.76 +    gen_abstract_domains ctxt dest thm
   76.77    end
   76.78  
   76.79  fun detect_transfer_rules thm =
   76.80 @@ -587,11 +587,11 @@
   76.81          handle TERM (_, ts) => raise TERM (err_msg, ts)
   76.82    in
   76.83      EVERY
   76.84 -      [rewrite_goal_tac pre_simps i THEN
   76.85 +      [rewrite_goal_tac ctxt pre_simps i THEN
   76.86         SUBGOAL main_tac i,
   76.87         (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
   76.88 -       rewrite_goal_tac post_simps i,
   76.89 -       Goal.norm_hhf_tac i]
   76.90 +       rewrite_goal_tac ctxt post_simps i,
   76.91 +       Goal.norm_hhf_tac ctxt i]
   76.92    end
   76.93  
   76.94  fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
   76.95 @@ -626,7 +626,7 @@
   76.96                  |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
   76.97      val thm2 = thm1
   76.98        |> Thm.certify_instantiate (instT, [])
   76.99 -      |> Raw_Simplifier.rewrite_rule pre_simps
  76.100 +      |> Raw_Simplifier.rewrite_rule ctxt pre_simps
  76.101      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
  76.102      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
  76.103      val rule = transfer_rule_of_lhs ctxt' t
  76.104 @@ -641,7 +641,7 @@
  76.105      val tnames = map (fst o dest_TFree o snd) instT
  76.106    in
  76.107      thm3
  76.108 -      |> Raw_Simplifier.rewrite_rule post_simps
  76.109 +      |> Raw_Simplifier.rewrite_rule ctxt' post_simps
  76.110        |> Raw_Simplifier.norm_hhf
  76.111        |> Drule.generalize (tnames, [])
  76.112        |> Drule.zero_var_indexes
  76.113 @@ -662,7 +662,7 @@
  76.114                  |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
  76.115      val thm2 = thm1
  76.116        |> Thm.certify_instantiate (instT, [])
  76.117 -      |> Raw_Simplifier.rewrite_rule pre_simps
  76.118 +      |> Raw_Simplifier.rewrite_rule ctxt pre_simps
  76.119      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
  76.120      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
  76.121      val rule = transfer_rule_of_term ctxt' true t
  76.122 @@ -677,7 +677,7 @@
  76.123      val tnames = map (fst o dest_TFree o snd) instT
  76.124    in
  76.125      thm3
  76.126 -      |> Raw_Simplifier.rewrite_rule post_simps
  76.127 +      |> Raw_Simplifier.rewrite_rule ctxt' post_simps
  76.128        |> Raw_Simplifier.norm_hhf
  76.129        |> Drule.generalize (tnames, [])
  76.130        |> Drule.zero_var_indexes
  76.131 @@ -700,8 +700,8 @@
  76.132  
  76.133  (* Attribute for transfer rules *)
  76.134  
  76.135 -fun prep_rule ctxt thm = 
  76.136 -  (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm
  76.137 +fun prep_rule ctxt = 
  76.138 +  abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
  76.139  
  76.140  val transfer_add =
  76.141    Thm.declaration_attribute (fn thm => fn ctxt => 
  76.142 @@ -742,10 +742,14 @@
  76.143  val relator_eq_setup =
  76.144    let
  76.145      val name = @{binding relator_eq}
  76.146 -    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
  76.147 -      #> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
  76.148 -    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
  76.149 -      #> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
  76.150 +    fun add_thm thm context = context
  76.151 +      |> Data.map (map_relator_eq (Item_Net.update thm))
  76.152 +      |> Data.map (map_relator_eq_raw
  76.153 +          (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
  76.154 +    fun del_thm thm context = context
  76.155 +      |> Data.map (map_relator_eq (Item_Net.remove thm))
  76.156 +      |> Data.map (map_relator_eq_raw
  76.157 +          (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
  76.158      val add = Thm.declaration_attribute add_thm
  76.159      val del = Thm.declaration_attribute del_thm
  76.160      val text = "declaration of relator equality rule (used by transfer method)"
    77.1 --- a/src/HOL/Word/Word.thy	Fri Dec 13 23:53:02 2013 +0100
    77.2 +++ b/src/HOL/Word/Word.thy	Sat Dec 14 17:28:05 2013 +0100
    77.3 @@ -1463,7 +1463,7 @@
    77.4          (put_simpset HOL_ss ctxt
    77.5            |> fold Splitter.add_split @{thms uint_splits}
    77.6            |> fold Simplifier.add_cong @{thms power_False_cong})),
    77.7 -      rewrite_goals_tac @{thms word_size}, 
    77.8 +      rewrite_goals_tac ctxt @{thms word_size}, 
    77.9        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
   77.10                           REPEAT (etac conjE n) THEN
   77.11                           REPEAT (dtac @{thm word_of_int_inverse} n 
   77.12 @@ -1964,7 +1964,7 @@
   77.13          (put_simpset HOL_ss ctxt
   77.14            |> fold Splitter.add_split @{thms unat_splits}
   77.15            |> fold Simplifier.add_cong @{thms power_False_cong})),
   77.16 -      rewrite_goals_tac @{thms word_size}, 
   77.17 +      rewrite_goals_tac ctxt @{thms word_size}, 
   77.18        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
   77.19                           REPEAT (etac conjE n) THEN
   77.20                           REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
    78.1 --- a/src/Provers/blast.ML	Fri Dec 13 23:53:02 2013 +0100
    78.2 +++ b/src/Provers/blast.ML	Sat Dec 14 17:28:05 2013 +0100
    78.3 @@ -1265,7 +1265,7 @@
    78.4  
    78.5  fun depth_tac ctxt lim i st =
    78.6    SELECT_GOAL
    78.7 -    (Object_Logic.atomize_prems_tac 1 THEN
    78.8 +    (Object_Logic.atomize_prems_tac ctxt 1 THEN
    78.9        raw_blast (Timing.start ()) ctxt lim) i st;
   78.10  
   78.11  fun blast_tac ctxt i st =
   78.12 @@ -1274,7 +1274,7 @@
   78.13      val lim = Config.get ctxt depth_limit;
   78.14    in
   78.15      SELECT_GOAL
   78.16 -     (Object_Logic.atomize_prems_tac 1 THEN
   78.17 +     (Object_Logic.atomize_prems_tac ctxt 1 THEN
   78.18        DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
   78.19    end;
   78.20  
    79.1 --- a/src/Provers/clasimp.ML	Fri Dec 13 23:53:02 2013 +0100
    79.2 +++ b/src/Provers/clasimp.ML	Sat Dec 14 17:28:05 2013 +0100
    79.3 @@ -150,7 +150,7 @@
    79.4      TRY (Classical.safe_tac ctxt) THEN
    79.5      REPEAT_DETERM (FIRSTGOAL main_tac) THEN
    79.6      TRY (Classical.safe_tac (addSss ctxt)) THEN
    79.7 -    prune_params_tac
    79.8 +    prune_params_tac ctxt
    79.9    end;
   79.10  
   79.11  fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
    80.1 --- a/src/Provers/classical.ML	Fri Dec 13 23:53:02 2013 +0100
    80.2 +++ b/src/Provers/classical.ML	Sat Dec 14 17:28:05 2013 +0100
    80.3 @@ -166,7 +166,13 @@
    80.4    else rule;
    80.5  
    80.6  (*flatten nested meta connectives in prems*)
    80.7 -val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
    80.8 +fun flat_rule opt_context th =
    80.9 +  let
   80.10 +    val ctxt =
   80.11 +      (case opt_context of
   80.12 +        NONE => Proof_Context.init_global (Thm.theory_of_thm th)
   80.13 +      | SOME context => Context.proof_of context);
   80.14 +  in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
   80.15  
   80.16  
   80.17  (*** Useful tactics for classical reasoning ***)
   80.18 @@ -325,7 +331,7 @@
   80.19    if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   80.20    else
   80.21      let
   80.22 -      val th' = flat_rule th;
   80.23 +      val th' = flat_rule context th;
   80.24        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   80.25          List.partition Thm.no_prems [th'];
   80.26        val nI = Item_Net.length safeIs + 1;
   80.27 @@ -354,7 +360,7 @@
   80.28      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   80.29    else
   80.30      let
   80.31 -      val th' = classical_rule (flat_rule th);
   80.32 +      val th' = classical_rule (flat_rule context th);
   80.33        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   80.34          List.partition (fn rl => nprems_of rl=1) [th'];
   80.35        val nI = Item_Net.length safeIs;
   80.36 @@ -386,7 +392,7 @@
   80.37    if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   80.38    else
   80.39      let
   80.40 -      val th' = flat_rule th;
   80.41 +      val th' = flat_rule context th;
   80.42        val nI = Item_Net.length hazIs + 1;
   80.43        val nE = Item_Net.length hazEs;
   80.44        val _ = warn_claset context th cs;
   80.45 @@ -415,7 +421,7 @@
   80.46      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   80.47    else
   80.48      let
   80.49 -      val th' = classical_rule (flat_rule th);
   80.50 +      val th' = classical_rule (flat_rule context th);
   80.51        val nI = Item_Net.length hazIs;
   80.52        val nE = Item_Net.length hazEs + 1;
   80.53        val _ = warn_claset context th cs;
   80.54 @@ -443,12 +449,12 @@
   80.55          to insert.
   80.56  ***)
   80.57  
   80.58 -fun delSI th
   80.59 +fun delSI context th
   80.60      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   80.61        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   80.62    if Item_Net.member safeIs th then
   80.63      let
   80.64 -      val th' = flat_rule th;
   80.65 +      val th' = flat_rule context th;
   80.66        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
   80.67      in
   80.68        CS
   80.69 @@ -466,12 +472,12 @@
   80.70      end
   80.71    else cs;
   80.72  
   80.73 -fun delSE th
   80.74 +fun delSE context th
   80.75      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   80.76        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   80.77    if Item_Net.member safeEs th then
   80.78      let
   80.79 -      val th' = classical_rule (flat_rule th);
   80.80 +      val th' = classical_rule (flat_rule context th);
   80.81        val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
   80.82      in
   80.83        CS
   80.84 @@ -493,7 +499,7 @@
   80.85      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   80.86        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   80.87    if Item_Net.member hazIs th then
   80.88 -    let val th' = flat_rule th in
   80.89 +    let val th' = flat_rule context th in
   80.90        CS
   80.91         {haz_netpair = delete ([th'], []) haz_netpair,
   80.92          dup_netpair = delete ([dup_intr th'], []) dup_netpair,
   80.93 @@ -511,11 +517,11 @@
   80.94    handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   80.95      error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
   80.96  
   80.97 -fun delE th
   80.98 +fun delE context th
   80.99      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
  80.100        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
  80.101    if Item_Net.member hazEs th then
  80.102 -    let val th' = classical_rule (flat_rule th) in
  80.103 +    let val th' = classical_rule (flat_rule context th) in
  80.104        CS
  80.105         {haz_netpair = delete ([], [th']) haz_netpair,
  80.106          dup_netpair = delete ([], [dup_elim th']) dup_netpair,
  80.107 @@ -537,7 +543,11 @@
  80.108      if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
  80.109        Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
  80.110        Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
  80.111 -    then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
  80.112 +    then
  80.113 +      delSI context th
  80.114 +        (delSE context th
  80.115 +          (delI context th
  80.116 +            (delE context th (delSE context th' (delE context th' cs)))))
  80.117      else (warn_thm context "Undeclared classical rule\n" th; cs)
  80.118    end;
  80.119  
  80.120 @@ -774,24 +784,24 @@
  80.121  
  80.122  (*Dumb but fast*)
  80.123  fun fast_tac ctxt =
  80.124 -  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
  80.125 +  Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
  80.126  
  80.127  (*Slower but smarter than fast_tac*)
  80.128  fun best_tac ctxt =
  80.129 -  Object_Logic.atomize_prems_tac THEN'
  80.130 +  Object_Logic.atomize_prems_tac ctxt THEN'
  80.131    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
  80.132  
  80.133  (*even a bit smarter than best_tac*)
  80.134  fun first_best_tac ctxt =
  80.135 -  Object_Logic.atomize_prems_tac THEN'
  80.136 +  Object_Logic.atomize_prems_tac ctxt THEN'
  80.137    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
  80.138  
  80.139  fun slow_tac ctxt =
  80.140 -  Object_Logic.atomize_prems_tac THEN'
  80.141 +  Object_Logic.atomize_prems_tac ctxt THEN'
  80.142    SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
  80.143  
  80.144  fun slow_best_tac ctxt =
  80.145 -  Object_Logic.atomize_prems_tac THEN'
  80.146 +  Object_Logic.atomize_prems_tac ctxt THEN'
  80.147    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
  80.148  
  80.149  
  80.150 @@ -800,13 +810,13 @@
  80.151  val weight_ASTAR = 5;
  80.152  
  80.153  fun astar_tac ctxt =
  80.154 -  Object_Logic.atomize_prems_tac THEN'
  80.155 +  Object_Logic.atomize_prems_tac ctxt THEN'
  80.156    SELECT_GOAL
  80.157      (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
  80.158        (step_tac ctxt 1));
  80.159  
  80.160  fun slow_astar_tac ctxt =
  80.161 -  Object_Logic.atomize_prems_tac THEN'
  80.162 +  Object_Logic.atomize_prems_tac ctxt THEN'
  80.163    SELECT_GOAL
  80.164      (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
  80.165        (slow_step_tac ctxt 1));
  80.166 @@ -901,12 +911,12 @@
  80.167    in
  80.168      fn st => Seq.maps (fn rule => rtac rule i st) ruleq
  80.169    end)
  80.170 -  THEN_ALL_NEW Goal.norm_hhf_tac;
  80.171 +  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
  80.172  
  80.173  in
  80.174  
  80.175  fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
  80.176 -  | rule_tac _ rules facts = Method.rule_tac rules facts;
  80.177 +  | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
  80.178  
  80.179  fun default_tac ctxt rules facts =
  80.180    HEADGOAL (rule_tac ctxt rules facts) ORELSE
  80.181 @@ -941,7 +951,7 @@
  80.182      (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
  80.183      "apply some intro/elim rule (potentially classical)" #>
  80.184    Method.setup @{binding contradiction}
  80.185 -    (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
  80.186 +    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
  80.187      "proof by contradiction" #>
  80.188    Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
  80.189      "repeatedly apply safe steps" #>
    81.1 --- a/src/Provers/splitter.ML	Fri Dec 13 23:53:02 2013 +0100
    81.2 +++ b/src/Provers/splitter.ML	Sat Dec 14 17:28:05 2013 +0100
    81.3 @@ -100,7 +100,7 @@
    81.4  val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
    81.5    [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
    81.6    (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
    81.7 -  (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
    81.8 +  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
    81.9  
   81.10  val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
   81.11  
    82.1 --- a/src/Pure/Isar/class.ML	Fri Dec 13 23:53:02 2013 +0100
    82.2 +++ b/src/Pure/Isar/class.ML	Sat Dec 14 17:28:05 2013 +0100
    82.3 @@ -656,7 +656,7 @@
    82.4    | default_intro_tac _ _ = no_tac;
    82.5  
    82.6  fun default_tac rules ctxt facts =
    82.7 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    82.8 +  HEADGOAL (Method.some_rule_tac ctxt rules facts) ORELSE
    82.9      default_intro_tac ctxt facts;
   82.10  
   82.11  val _ = Theory.setup
    83.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Dec 13 23:53:02 2013 +0100
    83.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Dec 14 17:28:05 2013 +0100
    83.3 @@ -58,7 +58,7 @@
    83.4              (_, NONE) => all_tac
    83.5            | (_, SOME intro) => ALLGOALS (rtac intro));
    83.6          val tac = loc_intro_tac
    83.7 -          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
    83.8 +          THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
    83.9        in Element.prove_witness empty_ctxt prop tac end) some_prop;
   83.10      val some_axiom = Option.map Element.conclude_witness some_witn;
   83.11  
   83.12 @@ -77,8 +77,10 @@
   83.13              SOME eq_morph => const_morph $> eq_morph
   83.14            | NONE => const_morph);
   83.15          val thm'' = Morphism.thm const_eq_morph thm';
   83.16 -        val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
   83.17 -      in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
   83.18 +      in
   83.19 +        Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
   83.20 +          (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
   83.21 +      end;
   83.22      val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
   83.23  
   83.24      (* of_class *)
    84.1 --- a/src/Pure/Isar/code.ML	Fri Dec 13 23:53:02 2013 +0100
    84.2 +++ b/src/Pure/Isar/code.ML	Sat Dec 14 17:28:05 2013 +0100
    84.3 @@ -1130,9 +1130,12 @@
    84.4      fun mk_prem z = Free (z, T_cong);
    84.5      fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
    84.6      val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
    84.7 -    fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
    84.8 -      THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
    84.9 -  in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
   84.10 +  in
   84.11 +    Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl
   84.12 +      (fn {context = ctxt', prems} =>
   84.13 +        Simplifier.rewrite_goals_tac ctxt' prems
   84.14 +        THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm]))
   84.15 +  end;
   84.16  
   84.17  fun add_case thm thy =
   84.18    let
    85.1 --- a/src/Pure/Isar/element.ML	Fri Dec 13 23:53:02 2013 +0100
    85.2 +++ b/src/Pure/Isar/element.ML	Sat Dec 14 17:28:05 2013 +0100
    85.3 @@ -456,11 +456,16 @@
    85.4  
    85.5  fun eq_morphism _ [] = NONE
    85.6    | eq_morphism thy thms =
    85.7 -      SOME (Morphism.morphism "Element.eq_morphism"
    85.8 -       {binding = [],
    85.9 -        typ = [],
   85.10 -        term = [Raw_Simplifier.rewrite_term thy thms []],
   85.11 -        fact = [map (rewrite_rule thms)]});
   85.12 +      let
   85.13 +        (* FIXME proper context!? *)
   85.14 +        fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
   85.15 +        val phi =
   85.16 +          Morphism.morphism "Element.eq_morphism"
   85.17 +           {binding = [],
   85.18 +            typ = [],
   85.19 +            term = [Raw_Simplifier.rewrite_term thy thms []],
   85.20 +            fact = [map rewrite]};
   85.21 +      in SOME phi end;
   85.22  
   85.23  
   85.24  
    86.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 13 23:53:02 2013 +0100
    86.2 +++ b/src/Pure/Isar/expression.ML	Sat Dec 14 17:28:05 2013 +0100
    86.3 @@ -619,7 +619,7 @@
    86.4      val bodyT = Term.fastype_of body;
    86.5    in
    86.6      if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
    86.7 -    else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
    86.8 +    else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
    86.9    end;
   86.10  
   86.11  (* achieve plain syntax for locale predicates (without "PROP") *)
   86.12 @@ -669,20 +669,22 @@
   86.13  
   86.14      val cert = Thm.cterm_of defs_thy;
   86.15  
   86.16 -    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
   86.17 -      rewrite_goals_tac [pred_def] THEN
   86.18 -      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   86.19 -      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   86.20 +    val intro = Goal.prove_global defs_thy [] norm_ts statement
   86.21 +      (fn {context = ctxt, ...} =>
   86.22 +        rewrite_goals_tac ctxt [pred_def] THEN
   86.23 +        compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   86.24 +        compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   86.25  
   86.26      val conjuncts =
   86.27 -      (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
   86.28 +      (Drule.equal_elim_rule2 OF
   86.29 +        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
   86.30        |> Conjunction.elim_balanced (length ts);
   86.31  
   86.32      val (_, axioms_ctxt) = defs_ctxt
   86.33        |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
   86.34      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   86.35        Element.prove_witness axioms_ctxt t
   86.36 -       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
   86.37 +       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
   86.38    in ((statement, intro, axioms), defs_thy) end;
   86.39  
   86.40  in
   86.41 @@ -849,7 +851,7 @@
   86.42      val dep_morphs = map2 (fn (dep, morph) => fn wits =>
   86.43        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
   86.44      fun activate' dep_morph ctxt = activate dep_morph
   86.45 -      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
   86.46 +        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
   86.47    in
   86.48      ctxt'
   86.49      |> fold activate' dep_morphs
    87.1 --- a/src/Pure/Isar/generic_target.ML	Fri Dec 13 23:53:02 2013 +0100
    87.2 +++ b/src/Pure/Isar/generic_target.ML	Sat Dec 14 17:28:05 2013 +0100
    87.3 @@ -104,7 +104,7 @@
    87.4      (*result*)
    87.5      val def =
    87.6        Thm.transitive local_def global_def
    87.7 -      |> Local_Defs.contract defs
    87.8 +      |> Local_Defs.contract lthy3 defs
    87.9            (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
   87.10      val ([(res_name, [res])], lthy4) = lthy3
   87.11        |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   87.12 @@ -125,7 +125,7 @@
   87.13      (*export assumes/defines*)
   87.14      val th = Goal.norm_result raw_th;
   87.15      val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
   87.16 -    val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
   87.17 +    val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
   87.18  
   87.19      (*export fixes*)
   87.20      val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
   87.21 @@ -153,7 +153,7 @@
   87.22      val result'' =
   87.23        (fold (curry op COMP) asms' result'
   87.24          handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
   87.25 -      |> Local_Defs.contract defs (Thm.cprop_of th)
   87.26 +      |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
   87.27        |> Goal.norm_result
   87.28        |> Global_Theory.name_thm false false name;
   87.29  
    88.1 --- a/src/Pure/Isar/local_defs.ML	Fri Dec 13 23:53:02 2013 +0100
    88.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Dec 14 17:28:05 2013 +0100
    88.3 @@ -17,7 +17,7 @@
    88.4      (term * term) * Proof.context
    88.5    val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
    88.6    val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm
    88.7 -  val contract: thm list -> cterm -> thm -> thm
    88.8 +  val contract: Proof.context -> thm list -> cterm -> thm -> thm
    88.9    val print_rules: Proof.context -> unit
   88.10    val defn_add: attribute
   88.11    val defn_del: attribute
   88.12 @@ -162,8 +162,8 @@
   88.13  fun export_cterm inner outer ct =
   88.14    export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
   88.15  
   88.16 -fun contract defs ct th =
   88.17 -  th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2);
   88.18 +fun contract ctxt defs ct th =
   88.19 +  th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2);
   88.20  
   88.21  
   88.22  
   88.23 @@ -200,7 +200,7 @@
   88.24  
   88.25  (* rewriting with object-level rules *)
   88.26  
   88.27 -fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
   88.28 +fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt);
   88.29  
   88.30  val unfold       = meta Raw_Simplifier.rewrite_rule;
   88.31  val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
   88.32 @@ -220,10 +220,12 @@
   88.33        |> conditional ? Logic.strip_imp_concl
   88.34        |> (abs_def o #2 o cert_def ctxt);
   88.35      fun prove ctxt' def =
   88.36 -      Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop (K (ALLGOALS
   88.37 -        (CONVERSION (meta_rewrite_conv ctxt') THEN'
   88.38 -          rewrite_goal_tac [def] THEN'
   88.39 -          resolve_tac [Drule.reflexive_thm])))
   88.40 +      Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop
   88.41 +        (fn {context = ctxt'', ...} =>
   88.42 +          ALLGOALS
   88.43 +            (CONVERSION (meta_rewrite_conv ctxt'') THEN'
   88.44 +              rewrite_goal_tac ctxt'' [def] THEN'
   88.45 +              resolve_tac [Drule.reflexive_thm]))
   88.46        handle ERROR msg => cat_error msg "Failed to prove definitional specification";
   88.47    in (((c, T), rhs), prove) end;
   88.48  
    89.1 --- a/src/Pure/Isar/method.ML	Fri Dec 13 23:53:02 2013 +0100
    89.2 +++ b/src/Pure/Isar/method.ML	Sat Dec 14 17:28:05 2013 +0100
    89.3 @@ -25,7 +25,7 @@
    89.4    val elim: thm list -> method
    89.5    val unfold: thm list -> Proof.context -> method
    89.6    val fold: thm list -> Proof.context -> method
    89.7 -  val atomize: bool -> method
    89.8 +  val atomize: bool -> Proof.context -> method
    89.9    val this: method
   89.10    val fact: thm list -> Proof.context -> method
   89.11    val assm_tac: Proof.context -> int -> tactic
   89.12 @@ -33,14 +33,14 @@
   89.13    val assumption: Proof.context -> method
   89.14    val rule_trace: bool Config.T
   89.15    val trace: Proof.context -> thm list -> unit
   89.16 -  val rule_tac: thm list -> thm list -> int -> tactic
   89.17 -  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
   89.18 +  val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
   89.19 +  val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
   89.20    val intros_tac: thm list -> thm list -> tactic
   89.21    val try_intros_tac: thm list -> thm list -> tactic
   89.22 -  val rule: thm list -> method
   89.23 -  val erule: int -> thm list -> method
   89.24 -  val drule: int -> thm list -> method
   89.25 -  val frule: int -> thm list -> method
   89.26 +  val rule: Proof.context -> thm list -> method
   89.27 +  val erule: Proof.context -> int -> thm list -> method
   89.28 +  val drule: Proof.context -> int -> thm list -> method
   89.29 +  val frule: Proof.context -> int -> thm list -> method
   89.30    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
   89.31    val tactic: string * Position.T -> Proof.context -> method
   89.32    val raw_tactic: string * Position.T -> Proof.context -> method
   89.33 @@ -147,8 +147,10 @@
   89.34  
   89.35  (* atomize rule statements *)
   89.36  
   89.37 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
   89.38 -  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
   89.39 +fun atomize false ctxt =
   89.40 +      SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
   89.41 +  | atomize true ctxt =
   89.42 +      RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
   89.43  
   89.44  
   89.45  (* this -- resolve facts directly *)
   89.46 @@ -159,7 +161,7 @@
   89.47  (* fact -- composition by facts from context *)
   89.48  
   89.49  fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
   89.50 -  | fact rules _ = SIMPLE_METHOD' (Proof_Context.fact_tac rules);
   89.51 +  | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
   89.52  
   89.53  
   89.54  (* assumption *)
   89.55 @@ -208,31 +210,31 @@
   89.56  
   89.57  local
   89.58  
   89.59 -fun gen_rule_tac tac rules facts =
   89.60 +fun gen_rule_tac tac ctxt rules facts =
   89.61    (fn i => fn st =>
   89.62      if null facts then tac rules i st
   89.63      else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
   89.64 -  THEN_ALL_NEW Goal.norm_hhf_tac;
   89.65 +  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
   89.66  
   89.67 -fun gen_arule_tac tac j rules facts =
   89.68 -  EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
   89.69 +fun gen_arule_tac tac ctxt j rules facts =
   89.70 +  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
   89.71  
   89.72 -fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
   89.73 +fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
   89.74    let
   89.75      val rules =
   89.76        if not (null arg_rules) then arg_rules
   89.77        else flat (Context_Rules.find_rules false facts goal ctxt)
   89.78 -  in trace ctxt rules; tac rules facts i end);
   89.79 +  in trace ctxt rules; tac ctxt rules facts i end);
   89.80  
   89.81 -fun meth tac x = METHOD (HEADGOAL o tac x);
   89.82 -fun meth' tac x y = METHOD (HEADGOAL o tac x y);
   89.83 +fun meth tac x y = METHOD (HEADGOAL o tac x y);
   89.84 +fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
   89.85  
   89.86  in
   89.87  
   89.88  val rule_tac = gen_rule_tac resolve_tac;
   89.89  val rule = meth rule_tac;
   89.90  val some_rule_tac = gen_some_rule_tac rule_tac;
   89.91 -val some_rule = meth' some_rule_tac;
   89.92 +val some_rule = meth some_rule_tac;
   89.93  
   89.94  val erule = meth' (gen_arule_tac eresolve_tac);
   89.95  val drule = meth' (gen_arule_tac dresolve_tac);
   89.96 @@ -390,9 +392,9 @@
   89.97  
   89.98  (* extra rule methods *)
   89.99  
  89.100 -fun xrule_meth m =
  89.101 +fun xrule_meth meth =
  89.102    Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
  89.103 -  (fn (n, ths) => K (m n ths));
  89.104 +  (fn (n, ths) => fn ctxt => meth ctxt n ths);
  89.105  
  89.106  
  89.107  (* outer parser *)
  89.108 @@ -451,9 +453,10 @@
  89.109      "repeatedly apply elimination rules" #>
  89.110    setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
  89.111    setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
  89.112 -  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
  89.113 +  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
  89.114      "present local premises as object-level statements" #>
  89.115 -  setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
  89.116 +  setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
  89.117 +    "apply some intro/elim rule" #>
  89.118    setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
  89.119    setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
  89.120    setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
    90.1 --- a/src/Pure/Isar/object_logic.ML	Fri Dec 13 23:53:02 2013 +0100
    90.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Dec 14 17:28:05 2013 +0100
    90.3 @@ -21,14 +21,14 @@
    90.4    val declare_atomize: attribute
    90.5    val declare_rulify: attribute
    90.6    val atomize_term: theory -> term -> term
    90.7 -  val atomize: conv
    90.8 -  val atomize_prems: conv
    90.9 -  val atomize_prems_tac: int -> tactic
   90.10 -  val full_atomize_tac: int -> tactic
   90.11 +  val atomize: Proof.context -> conv
   90.12 +  val atomize_prems: Proof.context -> conv
   90.13 +  val atomize_prems_tac: Proof.context -> int -> tactic
   90.14 +  val full_atomize_tac: Proof.context -> int -> tactic
   90.15    val rulify_term: theory -> term -> term
   90.16 -  val rulify_tac: int -> tactic
   90.17 -  val rulify: thm -> thm
   90.18 -  val rulify_no_asm: thm -> thm
   90.19 +  val rulify_tac: Proof.context -> int -> tactic
   90.20 +  val rulify: Proof.context -> thm -> thm
   90.21 +  val rulify_no_asm: Proof.context -> thm -> thm
   90.22    val rule_format: attribute
   90.23    val rule_format_no_asm: attribute
   90.24  end;
   90.25 @@ -182,32 +182,31 @@
   90.26  fun atomize_term thy =
   90.27    drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
   90.28  
   90.29 -fun atomize ct =
   90.30 -  Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   90.31 +fun atomize ctxt =
   90.32 +  Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
   90.33  
   90.34 -fun atomize_prems ct =
   90.35 +fun atomize_prems ctxt ct =
   90.36    if Logic.has_meta_prems (Thm.term_of ct) then
   90.37 -    Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
   90.38 -      (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
   90.39 +    Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize) ctxt ct
   90.40    else Conv.all_conv ct;
   90.41  
   90.42 -val atomize_prems_tac = CONVERSION atomize_prems;
   90.43 -val full_atomize_tac = CONVERSION atomize;
   90.44 +val atomize_prems_tac = CONVERSION o atomize_prems;
   90.45 +val full_atomize_tac = CONVERSION o atomize;
   90.46  
   90.47  
   90.48  (* rulify *)
   90.49  
   90.50  fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
   90.51 -fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   90.52 +fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
   90.53  
   90.54 -fun gen_rulify full thm =
   90.55 -  Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm
   90.56 -  |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
   90.57 +fun gen_rulify full ctxt =
   90.58 +  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
   90.59 +  #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
   90.60  
   90.61  val rulify = gen_rulify true;
   90.62  val rulify_no_asm = gen_rulify false;
   90.63  
   90.64 -val rule_format = Thm.rule_attribute (K rulify);
   90.65 -val rule_format_no_asm = Thm.rule_attribute (K rulify_no_asm);
   90.66 +val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
   90.67 +val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
   90.68  
   90.69  end;
    91.1 --- a/src/Pure/Isar/proof.ML	Fri Dec 13 23:53:02 2013 +0100
    91.2 +++ b/src/Pure/Isar/proof.ML	Sat Dec 14 17:28:05 2013 +0100
    91.3 @@ -443,18 +443,18 @@
    91.4  
    91.5  local
    91.6  
    91.7 -fun finish_tac 0 = K all_tac
    91.8 -  | finish_tac n =
    91.9 -      Goal.norm_hhf_tac THEN'
   91.10 +fun finish_tac _ 0 = K all_tac
   91.11 +  | finish_tac ctxt n =
   91.12 +      Goal.norm_hhf_tac ctxt THEN'
   91.13        SUBGOAL (fn (goal, i) =>
   91.14          if can Logic.unprotect (Logic.strip_assums_concl goal) then
   91.15 -          etac Drule.protectI i THEN finish_tac (n - 1) i
   91.16 -        else finish_tac (n - 1) (i + 1));
   91.17 +          etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
   91.18 +        else finish_tac ctxt (n - 1) (i + 1));
   91.19  
   91.20 -fun goal_tac rule =
   91.21 -  Goal.norm_hhf_tac THEN'
   91.22 +fun goal_tac ctxt rule =
   91.23 +  Goal.norm_hhf_tac ctxt THEN'
   91.24    rtac rule THEN'
   91.25 -  finish_tac (Thm.nprems_of rule);
   91.26 +  finish_tac ctxt (Thm.nprems_of rule);
   91.27  
   91.28  fun FINDGOAL tac st =
   91.29    let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
   91.30 @@ -465,7 +465,7 @@
   91.31  fun refine_goals print_rule inner raw_rules state =
   91.32    let
   91.33      val (outer, (_, goal)) = get_goal state;
   91.34 -    fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
   91.35 +    fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
   91.36    in
   91.37      raw_rules
   91.38      |> Proof_Context.goal_export inner outer
    92.1 --- a/src/Pure/Isar/proof_context.ML	Fri Dec 13 23:53:02 2013 +0100
    92.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Dec 14 17:28:05 2013 +0100
    92.3 @@ -110,7 +110,7 @@
    92.4      (term list list * (Proof.context -> Proof.context)) * Proof.context
    92.5    val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
    92.6      (term list list * (Proof.context -> Proof.context)) * Proof.context
    92.7 -  val fact_tac: thm list -> int -> tactic
    92.8 +  val fact_tac: Proof.context -> thm list -> int -> tactic
    92.9    val some_fact_tac: Proof.context -> int -> tactic
   92.10    val get_fact: Proof.context -> Facts.ref -> thm list
   92.11    val get_fact_single: Proof.context -> Facts.ref -> thm
   92.12 @@ -889,12 +889,12 @@
   92.13  
   92.14  in
   92.15  
   92.16 -fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
   92.17 +fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts;
   92.18  
   92.19  fun potential_facts ctxt prop =
   92.20    Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
   92.21  
   92.22 -fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
   92.23 +fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
   92.24  
   92.25  end;
   92.26  
   92.27 @@ -913,7 +913,7 @@
   92.28  
   92.29          val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
   92.30          fun prove_fact th =
   92.31 -          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
   92.32 +          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
   92.33          val results = map_filter (try prove_fact) (potential_facts ctxt prop');
   92.34          val res =
   92.35            (case distinct Thm.eq_thm_prop results of
    93.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Dec 13 23:53:02 2013 +0100
    93.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Dec 14 17:28:05 2013 +0100
    93.3 @@ -31,7 +31,7 @@
    93.4    val make_nested: term -> theory * term ->
    93.5      ((string * string list) * string list) list -> cases
    93.6    val apply: term list -> T -> T
    93.7 -  val consume: thm list -> thm list -> ('a * int) * thm ->
    93.8 +  val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
    93.9      (('a * (int * thm list)) * thm) Seq.seq
   93.10    val get_consumes: thm -> int
   93.11    val put_consumes: int option -> thm -> thm
   93.12 @@ -203,24 +203,24 @@
   93.13  
   93.14  local
   93.15  
   93.16 -fun unfold_prems n defs th =
   93.17 +fun unfold_prems ctxt n defs th =
   93.18    if null defs then th
   93.19 -  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
   93.20 +  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th;
   93.21  
   93.22 -fun unfold_prems_concls defs th =
   93.23 +fun unfold_prems_concls ctxt defs th =
   93.24    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   93.25    else
   93.26      Conv.fconv_rule
   93.27        (Conv.concl_conv ~1 (Conjunction.convs
   93.28 -        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
   93.29 +        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th;
   93.30  
   93.31  in
   93.32  
   93.33 -fun consume defs facts ((xx, n), th) =
   93.34 +fun consume ctxt defs facts ((xx, n), th) =
   93.35    let val m = Int.min (length facts, n) in
   93.36      th
   93.37 -    |> unfold_prems n defs
   93.38 -    |> unfold_prems_concls defs
   93.39 +    |> unfold_prems ctxt n defs
   93.40 +    |> unfold_prems_concls ctxt defs
   93.41      |> Drule.multi_resolve (take m facts)
   93.42      |> Seq.map (pair (xx, (n - m, drop m facts)))
   93.43    end;
    94.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Dec 13 23:53:02 2013 +0100
    94.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Dec 14 17:28:05 2013 +0100
    94.3 @@ -237,7 +237,9 @@
    94.4        Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
    94.5      fun try_thm thm =
    94.6        if Thm.no_prems thm then rtac thm 1 goal'
    94.7 -      else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
    94.8 +      else
    94.9 +        (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
   94.10 +          1 goal';
   94.11    in
   94.12      fn Internal (_, thm) =>
   94.13          if is_some (Seq.pull (try_thm thm))
    95.1 --- a/src/Pure/axclass.ML	Fri Dec 13 23:53:02 2013 +0100
    95.2 +++ b/src/Pure/axclass.ML	Sat Dec 14 17:28:05 2013 +0100
    95.3 @@ -291,11 +291,17 @@
    95.4  
    95.5  fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
    95.6  
    95.7 -fun unoverload thy = rewrite_rule (inst_thms thy);
    95.8 -fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy));
    95.9 +fun unoverload thy =
   95.10 +  rewrite_rule (Proof_Context.init_global thy) (inst_thms thy);
   95.11 +
   95.12 +fun overload thy =
   95.13 +  rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy));
   95.14  
   95.15 -fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
   95.16 -fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   95.17 +fun unoverload_conv thy =
   95.18 +  Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy);
   95.19 +
   95.20 +fun overload_conv thy =
   95.21 +  Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy));
   95.22  
   95.23  fun lookup_inst_param consts params (c, T) =
   95.24    (case get_inst_tyco consts (c, T) of
    96.1 --- a/src/Pure/goal.ML	Fri Dec 13 23:53:02 2013 +0100
    96.2 +++ b/src/Pure/goal.ML	Sat Dec 14 17:28:05 2013 +0100
    96.3 @@ -49,7 +49,7 @@
    96.4    val conjunction_tac: int -> tactic
    96.5    val precise_conjunction_tac: int -> int -> tactic
    96.6    val recover_conjunction_tac: tactic
    96.7 -  val norm_hhf_tac: int -> tactic
    96.8 +  val norm_hhf_tac: Proof.context -> int -> tactic
    96.9    val assume_rule_tac: Proof.context -> int -> tactic
   96.10  end;
   96.11  
   96.12 @@ -317,11 +317,11 @@
   96.13  
   96.14  (* hhf normal form *)
   96.15  
   96.16 -val norm_hhf_tac =
   96.17 +fun norm_hhf_tac ctxt =
   96.18    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   96.19    THEN' SUBGOAL (fn (t, i) =>
   96.20      if Drule.is_norm_hhf t then all_tac
   96.21 -    else rewrite_goal_tac Drule.norm_hhf_eqs i);
   96.22 +    else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
   96.23  
   96.24  
   96.25  (* non-atomic goal assumptions *)
   96.26 @@ -330,7 +330,7 @@
   96.27    | non_atomic (Const ("all", _) $ _) = true
   96.28    | non_atomic _ = false;
   96.29  
   96.30 -fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
   96.31 +fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
   96.32    let
   96.33      val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
   96.34      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    97.1 --- a/src/Pure/raw_simplifier.ML	Fri Dec 13 23:53:02 2013 +0100
    97.2 +++ b/src/Pure/raw_simplifier.ML	Sat Dec 14 17:28:05 2013 +0100
    97.3 @@ -57,13 +57,13 @@
    97.4    val setSolver: Proof.context * solver -> Proof.context
    97.5    val addSolver: Proof.context * solver -> Proof.context
    97.6  
    97.7 -  val rewrite_rule: thm list -> thm -> thm
    97.8 -  val rewrite_goals_rule: thm list -> thm -> thm
    97.9 -  val rewrite_goals_tac: thm list -> tactic
   97.10 -  val rewrite_goal_tac: thm list -> int -> tactic
   97.11 -  val prune_params_tac: tactic
   97.12 -  val fold_rule: thm list -> thm -> thm
   97.13 -  val fold_goals_tac: thm list -> tactic
   97.14 +  val rewrite_rule: Proof.context -> thm list -> thm -> thm
   97.15 +  val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
   97.16 +  val rewrite_goals_tac: Proof.context -> thm list -> tactic
   97.17 +  val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
   97.18 +  val prune_params_tac: Proof.context -> tactic
   97.19 +  val fold_rule: Proof.context -> thm list -> thm -> thm
   97.20 +  val fold_goals_tac: Proof.context -> thm list -> tactic
   97.21    val norm_hhf: thm -> thm
   97.22    val norm_hhf_protect: thm -> thm
   97.23  end;
   97.24 @@ -126,7 +126,7 @@
   97.25      (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
   97.26    val generic_rewrite_goal_tac: bool * bool * bool ->
   97.27      (Proof.context -> tactic) -> Proof.context -> int -> tactic
   97.28 -  val rewrite: bool -> thm list -> conv
   97.29 +  val rewrite: Proof.context -> bool -> thm list -> conv
   97.30  end;
   97.31  
   97.32  structure Raw_Simplifier: RAW_SIMPLIFIER =
   97.33 @@ -1366,12 +1366,12 @@
   97.34  val simple_prover =
   97.35    SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
   97.36  
   97.37 -fun rewrite _ [] ct = Thm.reflexive ct
   97.38 -  | rewrite full thms ct =
   97.39 +fun rewrite _ _ [] = Thm.reflexive
   97.40 +  | rewrite ctxt full thms =
   97.41        rewrite_cterm (full, false, false) simple_prover
   97.42 -        (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
   97.43 +        (empty_simpset ctxt addsimps thms);
   97.44  
   97.45 -val rewrite_rule = Conv.fconv_rule o rewrite true;
   97.46 +fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
   97.47  
   97.48  (*simple term rewriting -- no proof*)
   97.49  fun rewrite_term thy rules procs =
   97.50 @@ -1380,15 +1380,15 @@
   97.51  fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
   97.52  
   97.53  (*Rewrite the subgoals of a proof state (represented by a theorem)*)
   97.54 -fun rewrite_goals_rule thms th =
   97.55 +fun rewrite_goals_rule ctxt thms th =
   97.56    Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
   97.57 -    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
   97.58 +    (empty_simpset ctxt addsimps thms))) th;
   97.59  
   97.60  
   97.61  (** meta-rewriting tactics **)
   97.62  
   97.63  (*Rewrite all subgoals*)
   97.64 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   97.65 +fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
   97.66  
   97.67  (*Rewrite one subgoal*)
   97.68  fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
   97.69 @@ -1396,12 +1396,12 @@
   97.70      Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
   97.71    else Seq.empty;
   97.72  
   97.73 -fun rewrite_goal_tac rews i st =
   97.74 +fun rewrite_goal_tac ctxt rews =
   97.75    generic_rewrite_goal_tac (true, false, false) (K no_tac)
   97.76 -    (global_context (Thm.theory_of_thm st) empty_ss addsimps rews) i st;
   97.77 +    (empty_simpset ctxt addsimps rews);
   97.78  
   97.79  (*Prunes all redundant parameters from the proof state by rewriting.*)
   97.80 -val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
   97.81 +fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
   97.82  
   97.83  
   97.84  (* for folding definitions, handling critical pairs *)
   97.85 @@ -1422,8 +1422,8 @@
   97.86  
   97.87  val rev_defs = sort_lhs_depths o map Thm.symmetric;
   97.88  
   97.89 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
   97.90 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   97.91 +fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
   97.92 +fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
   97.93  
   97.94  
   97.95  (* HHF normal form: !! before ==>, outermost !! generalized *)
    98.1 --- a/src/Sequents/S4.thy	Fri Dec 13 23:53:02 2013 +0100
    98.2 +++ b/src/Sequents/S4.thy	Sat Dec 14 17:28:05 2013 +0100
    98.3 @@ -43,7 +43,8 @@
    98.4  )
    98.5  *}
    98.6  
    98.7 -method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *}
    98.8 +method_setup S4_solve =
    98.9 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2)) *}
   98.10  
   98.11  
   98.12  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    99.1 --- a/src/Sequents/S43.thy	Fri Dec 13 23:53:02 2013 +0100
    99.2 +++ b/src/Sequents/S43.thy	Sat Dec 14 17:28:05 2013 +0100
    99.3 @@ -90,8 +90,8 @@
    99.4  
    99.5  
    99.6  method_setup S43_solve = {*
    99.7 -  Scan.succeed (K (SIMPLE_METHOD
    99.8 -    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
    99.9 +  Scan.succeed (fn ctxt => SIMPLE_METHOD
   99.10 +    (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3))
   99.11  *}
   99.12  
   99.13  
   100.1 --- a/src/Sequents/T.thy	Fri Dec 13 23:53:02 2013 +0100
   100.2 +++ b/src/Sequents/T.thy	Sat Dec 14 17:28:05 2013 +0100
   100.3 @@ -42,7 +42,7 @@
   100.4  )
   100.5  *}
   100.6  
   100.7 -method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
   100.8 +method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *}
   100.9  
  100.10  
  100.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   101.1 --- a/src/Sequents/modal.ML	Fri Dec 13 23:53:02 2013 +0100
   101.2 +++ b/src/Sequents/modal.ML	Sat Dec 14 17:28:05 2013 +0100
   101.3 @@ -19,7 +19,7 @@
   101.4      val rule_tac   : thm list -> int ->tactic
   101.5      val step_tac   : int -> tactic
   101.6      val solven_tac : int -> int -> tactic
   101.7 -    val solve_tac  : int -> tactic
   101.8 +    val solve_tac  : Proof.context -> int -> tactic
   101.9  end;
  101.10  
  101.11  functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
  101.12 @@ -78,7 +78,7 @@
  101.13                   ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
  101.14                     (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
  101.15  
  101.16 -fun solve_tac d = rewrite_goals_tac Modal_Rule.rewrite_rls THEN solven_tac d 1;
  101.17 +fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
  101.18  
  101.19  fun step_tac n = 
  101.20      COND (has_fewer_prems 1) all_tac 
   102.1 --- a/src/Tools/atomize_elim.ML	Fri Dec 13 23:53:02 2013 +0100
   102.2 +++ b/src/Tools/atomize_elim.ML	Sat Dec 14 17:28:05 2013 +0100
   102.3 @@ -59,8 +59,8 @@
   102.4     (EX x y z. ...) | ... | (EX a b c. ...)
   102.5  *)
   102.6  fun atomize_elim_conv ctxt ct =
   102.7 -    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
   102.8 -    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
   102.9 +    (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
  102.10 +    then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
  102.11      then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
  102.12                           then all_conv ct'
  102.13                           else raise CTERM ("atomize_elim", [ct', ct])))
   103.1 --- a/src/Tools/case_product.ML	Fri Dec 13 23:53:02 2013 +0100
   103.2 +++ b/src/Tools/case_product.ML	Sat Dec 14 17:28:05 2013 +0100
   103.3 @@ -65,14 +65,14 @@
   103.4      (concl, prems)
   103.5    end
   103.6  
   103.7 -fun case_product_tac prems struc thm1 thm2 =
   103.8 +fun case_product_tac ctxt prems struc thm1 thm2 =
   103.9    let
  103.10      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
  103.11      val thm2' = thm2 OF p_cons2
  103.12    in
  103.13      rtac (thm1 OF p_cons1)
  103.14       THEN' EVERY' (map (fn p =>
  103.15 -       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
  103.16 +       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
  103.17    end
  103.18  
  103.19  fun combine ctxt thm1 thm2 =
  103.20 @@ -80,8 +80,9 @@
  103.21      val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
  103.22      val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
  103.23    in
  103.24 -    Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
  103.25 -      case_product_tac prems prems_rich i_thm1 i_thm2 1)
  103.26 +    Goal.prove ctxt' [] (flat prems_rich) concl
  103.27 +      (fn {context = ctxt'', prems} =>
  103.28 +        case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1)
  103.29      |> singleton (Variable.export ctxt' ctxt)
  103.30    end
  103.31  
   104.1 --- a/src/Tools/coherent.ML	Fri Dec 13 23:53:02 2013 +0100
   104.2 +++ b/src/Tools/coherent.ML	Sat Dec 14 17:28:05 2013 +0100
   104.3 @@ -41,14 +41,14 @@
   104.4  
   104.5  val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
   104.6  
   104.7 -fun rulify_elim_conv ct =
   104.8 +fun rulify_elim_conv ctxt ct =
   104.9    if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
  104.10    else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
  104.11      (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
  104.12 -     Raw_Simplifier.rewrite true (map Thm.symmetric
  104.13 +     Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
  104.14         [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
  104.15  
  104.16 -fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
  104.17 +fun rulify_elim ctxt th = Simplifier.norm_hhf (Conv.fconv_rule (rulify_elim_conv ctxt) th);
  104.18  
  104.19  (* Decompose elimination rule of the form
  104.20     A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
  104.21 @@ -66,9 +66,9 @@
  104.22         (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
  104.23    end;
  104.24  
  104.25 -fun mk_rule th =
  104.26 +fun mk_rule ctxt th =
  104.27    let
  104.28 -    val th' = rulify_elim th;
  104.29 +    val th' = rulify_elim ctxt th;
  104.30      val (prems, cases) = dest_elim (prop_of th')
  104.31    in (th', prems, cases) end;
  104.32  
  104.33 @@ -208,19 +208,19 @@
  104.34  
  104.35  (** external interface **)
  104.36  
  104.37 -fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
  104.38 -  rtac (rulify_elim_conv concl RS Drule.equal_elim_rule2) 1 THEN
  104.39 -  SUBPROOF (fn {prems = prems', concl, context, ...} =>
  104.40 +fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
  104.41 +  rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
  104.42 +  SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
  104.43      let val xs = map (term_of o #2) params @
  104.44 -      map (fn (_, s) => Free (s, the (Variable.default_type context s)))
  104.45 -        (rev (Variable.dest_fixes context))  (* FIXME !? *)
  104.46 +      map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
  104.47 +        (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
  104.48      in
  104.49 -      case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
  104.50 +      case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
  104.51             (mk_dom xs) Net.empty 0 0 of
  104.52           NONE => no_tac
  104.53         | SOME prf =>
  104.54 -           rtac (thm_of_cl_prf (Proof_Context.theory_of context) concl [] prf) 1
  104.55 -    end) context 1) ctxt;
  104.56 +           rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
  104.57 +    end) ctxt' 1) ctxt;
  104.58  
  104.59  val setup = Method.setup @{binding coherent}
  104.60    (Attrib.thms >> (fn rules => fn ctxt =>
   105.1 --- a/src/Tools/eqsubst.ML	Fri Dec 13 23:53:02 2013 +0100
   105.2 +++ b/src/Tools/eqsubst.ML	Sat Dec 14 17:28:05 2013 +0100
   105.3 @@ -328,7 +328,7 @@
   105.4      val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
   105.5      val preelimrule =
   105.6        RW_Inst.rw ctxt m rule pth
   105.7 -      |> (Seq.hd o prune_params_tac)
   105.8 +      |> (Seq.hd o prune_params_tac ctxt)
   105.9        |> Thm.permute_prems 0 ~1 (* put old asm first *)
  105.10        |> unfix_frees cfvs (* unfix any global params *)
  105.11        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   106.1 --- a/src/Tools/induct.ML	Fri Dec 13 23:53:02 2013 +0100
   106.2 +++ b/src/Tools/induct.ML	Sat Dec 14 17:28:05 2013 +0100
   106.3 @@ -60,16 +60,16 @@
   106.4    val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
   106.5      (term option list * thm list) * Proof.context
   106.6    val atomize_term: theory -> term -> term
   106.7 -  val atomize_cterm: conv
   106.8 -  val atomize_tac: int -> tactic
   106.9 -  val inner_atomize_tac: int -> tactic
  106.10 +  val atomize_cterm: Proof.context -> conv
  106.11 +  val atomize_tac: Proof.context -> int -> tactic
  106.12 +  val inner_atomize_tac: Proof.context -> int -> tactic
  106.13    val rulified_term: thm -> theory * term
  106.14 -  val rulify_tac: int -> tactic
  106.15 +  val rulify_tac: Proof.context -> int -> tactic
  106.16    val simplified_rule: Proof.context -> thm -> thm
  106.17    val simplify_tac: Proof.context -> int -> tactic
  106.18    val trivial_tac: int -> tactic
  106.19    val rotate_tac: int -> int -> int -> tactic
  106.20 -  val internalize: int -> thm -> thm
  106.21 +  val internalize: Proof.context -> int -> thm -> thm
  106.22    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
  106.23    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
  106.24      thm list -> int -> cases_tactic
  106.25 @@ -433,10 +433,10 @@
  106.26  
  106.27  fun mark_constraints n ctxt = Conv.fconv_rule
  106.28    (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
  106.29 -     (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
  106.30 +     (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
  106.31  
  106.32 -val unmark_constraints = Conv.fconv_rule
  106.33 -  (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
  106.34 +fun unmark_constraints ctxt =
  106.35 +  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
  106.36  
  106.37  
  106.38  (* simplify *)
  106.39 @@ -504,11 +504,11 @@
  106.40    in
  106.41      fn i => fn st =>
  106.42        ruleq
  106.43 -      |> Seq.maps (Rule_Cases.consume [] facts)
  106.44 +      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
  106.45        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  106.46          let
  106.47            val rule' = rule
  106.48 -            |> simp ? (simplified_rule' ctxt #> unmark_constraints);
  106.49 +            |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
  106.50          in
  106.51            CASES (Rule_Cases.make_common (thy,
  106.52                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
  106.53 @@ -532,12 +532,12 @@
  106.54    Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
  106.55    #> Object_Logic.drop_judgment thy;
  106.56  
  106.57 -val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
  106.58 +fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
  106.59  
  106.60 -val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
  106.61 +fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
  106.62  
  106.63 -val inner_atomize_tac =
  106.64 -  rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
  106.65 +fun inner_atomize_tac ctxt =
  106.66 +  rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt;
  106.67  
  106.68  
  106.69  (* rulify *)
  106.70 @@ -553,11 +553,11 @@
  106.71      val (As, B) = Logic.strip_horn (Thm.prop_of thm);
  106.72    in (thy, Logic.list_implies (map rulify As, rulify B)) end;
  106.73  
  106.74 -val rulify_tac =
  106.75 -  rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
  106.76 -  rewrite_goal_tac Induct_Args.rulify_fallback THEN'
  106.77 +fun rulify_tac ctxt =
  106.78 +  rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
  106.79 +  rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
  106.80    Goal.conjunction_tac THEN_ALL_NEW
  106.81 -  (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
  106.82 +  (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
  106.83  
  106.84  
  106.85  (* prepare rule *)
  106.86 @@ -565,9 +565,9 @@
  106.87  fun rule_instance ctxt inst rule =
  106.88    Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
  106.89  
  106.90 -fun internalize k th =
  106.91 +fun internalize ctxt k th =
  106.92    th |> Thm.permute_prems 0 k
  106.93 -  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
  106.94 +  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt));
  106.95  
  106.96  
  106.97  (* guess rule instantiation -- cannot handle pending goal parameters *)
  106.98 @@ -683,8 +683,10 @@
  106.99      | NONE => all_tac)
 106.100    end);
 106.101  
 106.102 -fun miniscope_tac p = CONVERSION o
 106.103 -  Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
 106.104 +fun miniscope_tac p =
 106.105 +  CONVERSION o
 106.106 +    Conv.params_conv p (fn ctxt =>
 106.107 +      Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
 106.108  
 106.109  in
 106.110  
 106.111 @@ -743,7 +745,7 @@
 106.112      val thy = Proof_Context.theory_of ctxt;
 106.113  
 106.114      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
 106.115 -    val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
 106.116 +    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
 106.117  
 106.118      fun inst_rule (concls, r) =
 106.119        (if null insts then `Rule_Cases.get r
 106.120 @@ -774,7 +776,7 @@
 106.121    in
 106.122      (fn i => fn st =>
 106.123        ruleq
 106.124 -      |> Seq.maps (Rule_Cases.consume (flat defs) facts)
 106.125 +      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
 106.126        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
 106.127          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
 106.128            (CONJUNCTS (ALLGOALS
 106.129 @@ -791,9 +793,9 @@
 106.130                   else
 106.131                     arbitrary_tac defs_ctxt k xs)
 106.132               end)
 106.133 -          THEN' inner_atomize_tac) j))
 106.134 -        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
 106.135 -            guess_instance ctxt (internalize more_consumes rule) i st'
 106.136 +          THEN' inner_atomize_tac defs_ctxt) j))
 106.137 +        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
 106.138 +            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
 106.139              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
 106.140              |> Seq.maps (fn rule' =>
 106.141                CASES (rule_cases ctxt rule' cases)
 106.142 @@ -802,7 +804,7 @@
 106.143      THEN_ALL_NEW_CASES
 106.144        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
 106.145          else K all_tac)
 106.146 -       THEN_ALL_NEW rulify_tac)
 106.147 +       THEN_ALL_NEW rulify_tac ctxt)
 106.148    end;
 106.149  
 106.150  val induct_tac = gen_induct_tac (K I);
 106.151 @@ -849,7 +851,7 @@
 106.152    in
 106.153      SUBGOAL_CASES (fn (goal, i) => fn st =>
 106.154        ruleq goal
 106.155 -      |> Seq.maps (Rule_Cases.consume [] facts)
 106.156 +      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
 106.157        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
 106.158          guess_instance ctxt rule i st
 106.159          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   107.1 --- a/src/Tools/induct_tacs.ML	Fri Dec 13 23:53:02 2013 +0100
   107.2 +++ b/src/Tools/induct_tacs.ML	Sat Dec 14 17:28:05 2013 +0100
   107.3 @@ -98,7 +98,7 @@
   107.4              (_, rule) :: _ => rule
   107.5            | [] => raise THM ("No induction rules", 0, [])));
   107.6  
   107.7 -    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
   107.8 +    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
   107.9      val _ = Method.trace ctxt [rule'];
  107.10  
  107.11      val concls = Logic.dest_conjunctions (Thm.concl_of rule);
   108.1 --- a/src/Tools/intuitionistic.ML	Fri Dec 13 23:53:02 2013 +0100
   108.2 +++ b/src/Tools/intuitionistic.ML	Sat Dec 14 17:28:05 2013 +0100
   108.3 @@ -89,7 +89,7 @@
   108.4    Method.setup name
   108.5      (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
   108.6        (fn opt_lim => fn ctxt =>
   108.7 -        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
   108.8 +        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
   108.9      "intuitionistic proof search";
  108.10  
  108.11  end;
   109.1 --- a/src/ZF/Tools/cartprod.ML	Fri Dec 13 23:53:02 2013 +0100
   109.2 +++ b/src/ZF/Tools/cartprod.ML	Sat Dec 14 17:28:05 2013 +0100
   109.3 @@ -51,9 +51,9 @@
   109.4    val mk_prod : typ * typ -> typ
   109.5    val mk_tuple : term -> typ -> term list -> term
   109.6    val pseudo_type : term -> typ
   109.7 -  val remove_split : thm -> thm
   109.8 +  val remove_split : Proof.context -> thm -> thm
   109.9    val split_const : typ -> term
  109.10 -  val split_rule_var : term * typ * thm -> thm
  109.11 +  val split_rule_var : Proof.context -> term * typ * thm -> thm
  109.12    end;
  109.13  
  109.14  
  109.15 @@ -100,18 +100,18 @@
  109.16    | mk_tuple pair T (t::_) = t;
  109.17  
  109.18  (*Attempts to remove occurrences of split, and pair-valued parameters*)
  109.19 -val remove_split = rewrite_rule [Pr.split_eq];
  109.20 +fun remove_split ctxt = rewrite_rule ctxt [Pr.split_eq];
  109.21  
  109.22  (*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
  109.23 -fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
  109.24 +fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
  109.25        let val T' = factors T1 ---> T2
  109.26            val newt = ap_split T1 T2 (Var(v,T'))
  109.27            val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
  109.28        in
  109.29 -          remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
  109.30 +          remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
  109.31                                             cterm newt)]) rl)
  109.32        end
  109.33 -  | split_rule_var (t,T,rl) = rl;
  109.34 +  | split_rule_var _ (t,T,rl) = rl;
  109.35  
  109.36  end;
  109.37  
   110.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Dec 13 23:53:02 2013 +0100
   110.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Dec 14 17:28:05 2013 +0100
   110.3 @@ -288,8 +288,8 @@
   110.4      Goal.prove_global thy1 [] []
   110.5        (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
   110.6        (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
   110.7 -      (fn _ => EVERY
   110.8 -        [rewrite_goals_tac [con_def],
   110.9 +      (fn {context = ctxt, ...} => EVERY
  110.10 +        [rewrite_goals_tac ctxt [con_def],
  110.11           rtac case_trans 1,
  110.12           REPEAT
  110.13             (resolve_tac [@{thm refl}, split_trans,
  110.14 @@ -353,9 +353,9 @@
  110.15        val ctxt = Proof_Context.init_global thy;
  110.16      in
  110.17        Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
  110.18 -        (fn _ => EVERY
  110.19 -         [rewrite_goals_tac con_defs,
  110.20 -          fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
  110.21 +        (fn {context = ctxt', ...} => EVERY
  110.22 +         [rewrite_goals_tac ctxt' con_defs,
  110.23 +          fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])
  110.24      end;
  110.25  
  110.26    val simps = case_eqns @ recursor_eqns;
   111.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Dec 13 23:53:02 2013 +0100
   111.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Dec 14 17:28:05 2013 +0100
   111.3 @@ -58,7 +58,7 @@
   111.4  val setup =
   111.5    Method.setup @{binding "ind_cases"}
   111.6      (Scan.lift (Scan.repeat1 Args.name_source) >>
   111.7 -      (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
   111.8 +      (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
   111.9      "dynamic case analysis on sets";
  111.10  
  111.11  
   112.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Dec 13 23:53:02 2013 +0100
   112.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Dec 14 17:28:05 2013 +0100
   112.3 @@ -214,7 +214,7 @@
   112.4  
   112.5    (*Type-checking is hardest aspect of proof;
   112.6      disjIn selects the correct disjunct after unfolding*)
   112.7 -  fun intro_tacsf disjIn =
   112.8 +  fun intro_tacsf disjIn ctxt =
   112.9      [DETERM (stac unfold 1),
  112.10       REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
  112.11       (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
  112.12 @@ -223,7 +223,7 @@
  112.13         backtracking may occur if the premises have extra variables!*)
  112.14       DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
  112.15       (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
  112.16 -     rewrite_goals_tac con_defs,
  112.17 +     rewrite_goals_tac ctxt con_defs,
  112.18       REPEAT (rtac @{thm refl} 2),
  112.19       (*Typechecking; this can fail*)
  112.20       if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
  112.21 @@ -246,7 +246,7 @@
  112.22      (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
  112.23      |> ListPair.map (fn (t, tacs) =>
  112.24        Goal.prove_global thy1 [] [] t
  112.25 -        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
  112.26 +        (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt)));
  112.27  
  112.28    (********)
  112.29    val dummy = writeln "  Proving the elimination rule...";
  112.30 @@ -255,9 +255,9 @@
  112.31    fun basic_elim_tac ctxt =
  112.32        REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
  112.33                  ORELSE' bound_hyp_subst_tac ctxt))
  112.34 -      THEN prune_params_tac
  112.35 +      THEN prune_params_tac ctxt
  112.36            (*Mutual recursion: collapse references to Part(D,h)*)
  112.37 -      THEN (PRIMITIVE (fold_rule part_rec_defs));
  112.38 +      THEN (PRIMITIVE (fold_rule ctxt part_rec_defs));
  112.39  
  112.40    (*Elimination*)
  112.41    val elim =
  112.42 @@ -337,8 +337,8 @@
  112.43       val quant_induct =
  112.44         Goal.prove_global thy1 [] ind_prems
  112.45           (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
  112.46 -         (fn {prems, ...} => EVERY
  112.47 -           [rewrite_goals_tac part_rec_defs,
  112.48 +         (fn {context = ctxt, prems} => EVERY
  112.49 +           [rewrite_goals_tac ctxt part_rec_defs,
  112.50              rtac (@{thm impI} RS @{thm allI}) 1,
  112.51              DETERM (etac raw_induct 1),
  112.52              (*Push Part inside Collect*)
  112.53 @@ -349,7 +349,7 @@
  112.54                some premise involves disjunction.*)
  112.55              REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
  112.56                                 ORELSE' (bound_hyp_subst_tac ctxt1))),
  112.57 -            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
  112.58 +            ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
  112.59  
  112.60       val dummy =
  112.61        if ! Ind_Syntax.trace then
  112.62 @@ -422,9 +422,9 @@
  112.63            (writeln "  Proving the mutual induction rule...";
  112.64             Goal.prove_global thy1 [] []
  112.65               (Logic.mk_implies (induct_concl, mutual_induct_concl))
  112.66 -             (fn _ => EVERY
  112.67 -               [rewrite_goals_tac part_rec_defs,
  112.68 -                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
  112.69 +             (fn {context = ctxt, ...} => EVERY
  112.70 +               [rewrite_goals_tac ctxt part_rec_defs,
  112.71 +                REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac 1)]))
  112.72         else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
  112.73  
  112.74       val dummy =
  112.75 @@ -452,15 +452,15 @@
  112.76                     RLN (2,[@{thm rev_subsetD}]);
  112.77  
  112.78       (*Minimizes backtracking by delivering the correct premise to each goal*)
  112.79 -     fun mutual_ind_tac [] 0 = all_tac
  112.80 -       | mutual_ind_tac(prem::prems) i =
  112.81 +     fun mutual_ind_tac _ [] 0 = all_tac
  112.82 +       | mutual_ind_tac ctxt (prem::prems) i =
  112.83             DETERM
  112.84              (SELECT_GOAL
  112.85                 (
  112.86                  (*Simplify the assumptions and goal by unfolding Part and
  112.87                    using freeness of the Sum constructors; proves all but one
  112.88                    conjunct by contradiction*)
  112.89 -                rewrite_goals_tac all_defs  THEN
  112.90 +                rewrite_goals_tac ctxt all_defs  THEN
  112.91                  simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1  THEN
  112.92                  IF_UNSOLVED (*simp_tac may have finished it off!*)
  112.93                    ((*simplify assumptions*)
  112.94 @@ -471,20 +471,20 @@
  112.95                     THEN
  112.96                     (*unpackage and use "prem" in the corresponding place*)
  112.97                     REPEAT (rtac @{thm impI} 1)  THEN
  112.98 -                   rtac (rewrite_rule all_defs prem) 1  THEN
  112.99 +                   rtac (rewrite_rule ctxt all_defs prem) 1  THEN
 112.100                     (*prem must not be REPEATed below: could loop!*)
 112.101                     DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
 112.102                                             eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
 112.103                 ) i)
 112.104 -            THEN mutual_ind_tac prems (i-1);
 112.105 +            THEN mutual_ind_tac ctxt prems (i-1);
 112.106  
 112.107       val mutual_induct_fsplit =
 112.108         if need_mutual then
 112.109           Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
 112.110             mutual_induct_concl
 112.111 -           (fn {prems, ...} => EVERY
 112.112 +           (fn {context = ctxt, prems} => EVERY
 112.113               [rtac (quant_induct RS lemma) 1,
 112.114 -              mutual_ind_tac (rev prems) (length prems)])
 112.115 +              mutual_ind_tac ctxt (rev prems) (length prems)])
 112.116         else @{thm TrueI};
 112.117  
 112.118       (** Uncurrying the predicate in the ordinary induction rule **)
 112.119 @@ -502,9 +502,11 @@
 112.120  
 112.121       val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
 112.122  
 112.123 -     val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
 112.124 -                  |> Drule.export_without_context
 112.125 -     and mutual_induct = CP.remove_split mutual_induct_fsplit
 112.126 +     val induct =
 112.127 +       CP.split_rule_var (Proof_Context.init_global thy)
 112.128 +        (pred_var, elem_type-->FOLogic.oT, induct0)
 112.129 +       |> Drule.export_without_context
 112.130 +     and mutual_induct = CP.remove_split (Proof_Context.init_global thy) mutual_induct_fsplit
 112.131  
 112.132       val ([induct', mutual_induct'], thy') =
 112.133         thy
   113.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Dec 13 23:53:02 2013 +0100
   113.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Dec 14 17:28:05 2013 +0100
   113.3 @@ -176,7 +176,7 @@
   113.4      val eqn_thms =
   113.5        eqn_terms |> map (fn t =>
   113.6          Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
   113.7 -          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
   113.8 +          (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
   113.9  
  113.10      val (eqn_thms', thy2) =
  113.11        thy1
   114.1 --- a/src/ZF/UNITY/Constrains.thy	Fri Dec 13 23:53:02 2013 +0100
   114.2 +++ b/src/ZF/UNITY/Constrains.thy	Sat Dec 14 17:28:05 2013 +0100
   114.3 @@ -479,7 +479,7 @@
   114.4                                     @{thm constrains_imp_Constrains}] 1),
   114.5                rtac @{thm constrainsI} 1,
   114.6                (* Three subgoals *)
   114.7 -              rewrite_goal_tac [@{thm st_set_def}] 3,
   114.8 +              rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
   114.9                REPEAT (force_tac ctxt 2),
  114.10                full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
  114.11                ALLGOALS (clarify_tac ctxt),