proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
authorwenzelm
Sun Nov 09 14:08:00 2014 +0100 (2014-11-09)
changeset 58956a816aa3ff391
parent 58955 1694bad18568
child 58957 c9e744ea8a38
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
NEWS
src/Doc/Implementation/Tactic.thy
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/HOLCF/Tr.thy
src/HOL/Library/simps_case_conv.ML
src/HOL/List.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/record.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_test.thy
src/Provers/blast.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Pure/Isar/expression.ML
src/Pure/Tools/rule_insts.ML
src/Pure/tactic.ML
src/Tools/atomize_elim.ML
src/Tools/cong_tac.ML
src/Tools/induct.ML
     1.1 --- a/NEWS	Sun Nov 09 11:05:20 2014 +0100
     1.2 +++ b/NEWS	Sun Nov 09 14:08:00 2014 +0100
     1.3 @@ -190,6 +190,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Proper context for various elementary tactics: compose_tac,
     1.8 +Splitter.split_tac etc.  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
    1.11  PARALLEL_GOALS.
    1.12  
     2.1 --- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 11:05:20 2014 +0100
     2.2 +++ b/src/Doc/Implementation/Tactic.thy	Sun Nov 09 14:08:00 2014 +0100
     2.3 @@ -492,14 +492,14 @@
     2.4  
     2.5  text %mlref \<open>
     2.6    \begin{mldecls}
     2.7 -  @{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
     2.8 +  @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
     2.9    @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
    2.10    @{index_ML_op COMP: "thm * thm -> thm"} \\
    2.11    \end{mldecls}
    2.12  
    2.13    \begin{description}
    2.14  
    2.15 -  \item @{ML compose_tac}~@{text "(flag, rule, m) i"} refines subgoal
    2.16 +  \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
    2.17    @{text "i"} using @{text "rule"}, without lifting.  The @{text
    2.18    "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
    2.19    @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
     3.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 11:05:20 2014 +0100
     3.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 14:08:00 2014 +0100
     3.3 @@ -47,7 +47,7 @@
     3.4  
     3.5  fun linr_tac ctxt q =
     3.6      Object_Logic.atomize_prems_tac ctxt
     3.7 -        THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
     3.8 +        THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
     3.9          THEN' SUBGOAL (fn (g, i) =>
    3.10    let
    3.11      val thy = Proof_Context.theory_of ctxt
     4.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 09 11:05:20 2014 +0100
     4.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 09 14:08:00 2014 +0100
     4.3 @@ -67,7 +67,7 @@
     4.4      Object_Logic.atomize_prems_tac ctxt
     4.5          THEN' simp_tac (put_simpset HOL_basic_ss ctxt
     4.6            addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
     4.7 -        THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
     4.8 +        THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
     4.9          THEN' SUBGOAL (fn (g, i) =>
    4.10    let
    4.11      val thy = Proof_Context.theory_of ctxt
     5.1 --- a/src/HOL/HOL.thy	Sun Nov 09 11:05:20 2014 +0100
     5.2 +++ b/src/HOL/HOL.thy	Sun Nov 09 14:08:00 2014 +0100
     5.3 @@ -274,7 +274,7 @@
     5.4  apply (rule refl)
     5.5  done
     5.6  
     5.7 -ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
     5.8 +ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *}
     5.9  
    5.10  
    5.11  subsubsection {* Equality of booleans -- iff *}
     6.1 --- a/src/HOL/HOLCF/Tr.thy	Sun Nov 09 11:05:20 2014 +0100
     6.2 +++ b/src/HOL/HOLCF/Tr.thy	Sun Nov 09 14:08:00 2014 +0100
     6.3 @@ -154,7 +154,7 @@
     6.4  ML {*
     6.5  fun split_If_tac ctxt =
     6.6    simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
     6.7 -    THEN' (split_tac [@{thm split_If2}])
     6.8 +    THEN' (split_tac ctxt [@{thm split_If2}])
     6.9  *}
    6.10  
    6.11  subsection "Rewriting of HOLCF operations to HOL functions"
     7.1 --- a/src/HOL/Library/simps_case_conv.ML	Sun Nov 09 11:05:20 2014 +0100
     7.2 +++ b/src/HOL/Library/simps_case_conv.ML	Sun Nov 09 14:08:00 2014 +0100
     7.3 @@ -88,7 +88,7 @@
     7.4  
     7.5  fun tac ctxt {splits, intros, defs} =
     7.6    let val ctxt' = Classical.addSIs (ctxt, intros) in
     7.7 -    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
     7.8 +    REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt splits))
     7.9      THEN Local_Defs.unfold_tac ctxt defs
    7.10      THEN safe_tac ctxt'
    7.11    end
     8.1 --- a/src/HOL/List.thy	Sun Nov 09 11:05:20 2014 +0100
     8.2 +++ b/src/HOL/List.thy	Sun Nov 09 14:08:00 2014 +0100
     8.3 @@ -610,7 +610,7 @@
     8.4        | dest_if _ = NONE
     8.5      fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
     8.6        | tac ctxt (If :: cont) =
     8.7 -          Splitter.split_tac [@{thm split_if}] 1
     8.8 +          Splitter.split_tac ctxt [@{thm split_if}] 1
     8.9            THEN rtac @{thm conjI} 1
    8.10            THEN rtac @{thm impI} 1
    8.11            THEN Subgoal.FOCUS (fn {prems, context, ...} =>
    8.12 @@ -631,7 +631,7 @@
    8.13                Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
    8.14            in
    8.15              (* do case distinction *)
    8.16 -            Splitter.split_tac [split] 1
    8.17 +            Splitter.split_tac ctxt [split] 1
    8.18              THEN EVERY (map_index (fn (i', _) =>
    8.19                (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
    8.20                THEN REPEAT_DETERM (rtac @{thm allI} 1)
     9.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 09 11:05:20 2014 +0100
     9.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 09 14:08:00 2014 +0100
     9.3 @@ -654,7 +654,7 @@
     9.4                  ((Rep RS perm_closed1 RS Abs_inverse) ::
     9.5                   (if atom1 = atom2 then []
     9.6                    else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
     9.7 -              cong_tac 1,
     9.8 +              cong_tac ctxt 1,
     9.9                rtac refl 1,
    9.10                rtac cp1' 1]) thy)
    9.11          (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
    10.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Nov 09 11:05:20 2014 +0100
    10.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Nov 09 14:08:00 2014 +0100
    10.3 @@ -10,7 +10,7 @@
    10.4  (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
    10.5  
    10.6  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
    10.7 -fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
    10.8 +fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
    10.9    let
   10.10      val thy = theory_of_thm st;
   10.11      val cgoal = nth (cprems_of st) (i - 1);
   10.12 @@ -27,18 +27,18 @@
   10.13        (map (pairself (cterm_of thy)) tinst')
   10.14        (Thm.lift_rule cgoal th)
   10.15    in
   10.16 -    compose_tac (elim, th', nprems_of th) i st
   10.17 +    compose_tac ctxt (elim, th', nprems_of th) i st
   10.18    end handle General.Subscript => Seq.empty;
   10.19  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
   10.20  
   10.21 -val res_inst_tac_term =
   10.22 -  gen_res_inst_tac_term (curry Thm.instantiate);
   10.23 +fun res_inst_tac_term ctxt =
   10.24 +  gen_res_inst_tac_term ctxt (curry Thm.instantiate);
   10.25  
   10.26 -val res_inst_tac_term' =
   10.27 -  gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
   10.28 +fun res_inst_tac_term' ctxt =
   10.29 +  gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) [];
   10.30  
   10.31  fun cut_inst_tac_term' ctxt tinst th =
   10.32 -  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th);
   10.33 +  res_inst_tac_term' ctxt tinst false (Rule_Insts.make_elim_preserve ctxt th);
   10.34  
   10.35  fun get_dyn_thm thy name atom_name =
   10.36    Global_Theory.get_thm thy name handle ERROR _ =>
    11.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sun Nov 09 11:05:20 2014 +0100
    11.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Nov 09 14:08:00 2014 +0100
    11.3 @@ -227,7 +227,7 @@
    11.4        asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
    11.5        asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
    11.6  
    11.7 -fun apply_cong_tac i = ("application of congruence", cong_tac i);
    11.8 +fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
    11.9  
   11.10  
   11.11  (* unfolds the definition of permutations     *)
   11.12 @@ -256,7 +256,7 @@
   11.13                 (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i),
   11.14                         fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
   11.15                         fn i => tactical ctxt (perm_compose_tac ctxt i),
   11.16 -                       fn i => tactical ctxt (apply_cong_tac i), 
   11.17 +                       fn i => tactical ctxt (apply_cong_tac ctxt i), 
   11.18                         fn i => tactical ctxt (unfold_perm_fun_def_tac i),
   11.19                         fn i => tactical ctxt (ext_fun_tac i)]
   11.20                        THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
   11.21 @@ -315,7 +315,7 @@
   11.22              val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
   11.23            in
   11.24              (tactical ctxt ("guessing of the right supports-set",
   11.25 -                      EVERY [compose_tac (false, supports_rule'', 2) i,
   11.26 +                      EVERY [compose_tac ctxt (false, supports_rule'', 2) i,
   11.27                               asm_full_simp_tac ctxt' (i+1),
   11.28                               supports_tac_i tactical ctxt i])) st
   11.29            end
   11.30 @@ -357,7 +357,7 @@
   11.31                [(cert (head_of S), cert s')] supports_fresh_rule'
   11.32            in
   11.33              (tactical ctxt ("guessing of the right set that supports the goal", 
   11.34 -                      (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
   11.35 +                      (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
   11.36                               asm_full_simp_tac ctxt1 (i+2),
   11.37                               asm_full_simp_tac ctxt2 (i+1), 
   11.38                               supports_tac_i tactical ctxt i]))) st
    12.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Nov 09 11:05:20 2014 +0100
    12.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Nov 09 14:08:00 2014 +0100
    12.3 @@ -376,7 +376,7 @@
    12.4      Proof.apply (Method.Basic (fn ctxt => fn _ =>
    12.5        NO_CASES
    12.6         (rewrite_goals_tac ctxt defs_thms THEN
    12.7 -        compose_tac (false, rule, length rule_prems) 1))) |>
    12.8 +        compose_tac ctxt (false, rule, length rule_prems) 1))) |>
    12.9      Seq.hd
   12.10    end;
   12.11  
    13.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Nov 09 11:05:20 2014 +0100
    13.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Nov 09 14:08:00 2014 +0100
    13.3 @@ -209,7 +209,7 @@
    13.4        (fn _ =>
    13.5           rtac @{thm subset_antisym} 1 THEN
    13.6           rtac @{thm subsetI} 1 THEN
    13.7 -         Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
    13.8 +         Old_Datatype_Aux.exh_tac lthy (K (#exhaust (BNF_LFP_Compat.the_info
    13.9             (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
   13.10           ALLGOALS (asm_full_simp_tac lthy));
   13.11  
    14.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Nov 09 11:05:20 2014 +0100
    14.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Nov 09 14:08:00 2014 +0100
    14.3 @@ -133,8 +133,8 @@
    14.4    HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
    14.5      eresolve_tac falseEs ORELSE'
    14.6      resolve_tac split_connectI ORELSE'
    14.7 -    Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    14.8 -    Splitter.split_tac (split_if :: splits) ORELSE'
    14.9 +    Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
   14.10 +    Splitter.split_tac ctxt (split_if :: splits) ORELSE'
   14.11      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
   14.12      etac notE THEN' atac ORELSE'
   14.13      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
   14.14 @@ -171,8 +171,8 @@
   14.15        SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
   14.16        (rtac refl ORELSE' atac ORELSE'
   14.17         resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
   14.18 -       Splitter.split_tac (split_if :: splits) ORELSE'
   14.19 -       Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
   14.20 +       Splitter.split_tac ctxt (split_if :: splits) ORELSE'
   14.21 +       Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
   14.22         mk_primcorec_assumption_tac ctxt discIs ORELSE'
   14.23         distinct_in_prems_tac distincts ORELSE'
   14.24         (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
   14.25 @@ -204,7 +204,7 @@
   14.26      SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
   14.27      (rtac refl ORELSE' atac ORELSE'
   14.28       resolve_tac split_connectI ORELSE'
   14.29 -     Splitter.split_tac (split_if :: splits) ORELSE'
   14.30 +     Splitter.split_tac ctxt (split_if :: splits) ORELSE'
   14.31       distinct_in_prems_tac distincts ORELSE'
   14.32       rtac sym THEN' atac ORELSE'
   14.33       etac notE THEN' atac));
    15.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 09 11:05:20 2014 +0100
    15.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 09 14:08:00 2014 +0100
    15.3 @@ -421,7 +421,7 @@
    15.4                [(Old_Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
    15.5                 REPEAT (EVERY
    15.6                   [rtac allI 1, rtac impI 1,
    15.7 -                  Old_Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
    15.8 +                  Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1,
    15.9                    REPEAT (EVERY
   15.10                      [hyp_subst_tac ctxt 1,
   15.11                       rewrite_goals_tac ctxt rewrites,
   15.12 @@ -430,7 +430,7 @@
   15.13                       ORELSE (EVERY
   15.14                         [REPEAT (eresolve_tac (Scons_inject ::
   15.15                            map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
   15.16 -                        REPEAT (cong_tac 1), rtac refl 1,
   15.17 +                        REPEAT (cong_tac ctxt 1), rtac refl 1,
   15.18                          REPEAT (atac 1 ORELSE (EVERY
   15.19                            [REPEAT (rtac @{thm ext} 1),
   15.20                             REPEAT (eresolve_tac (mp :: allE ::
    16.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sun Nov 09 11:05:20 2014 +0100
    16.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sun Nov 09 14:08:00 2014 +0100
    16.3 @@ -53,7 +53,7 @@
    16.4    val app_bnds : term -> int -> term
    16.5  
    16.6    val ind_tac : thm -> string list -> int -> tactic
    16.7 -  val exh_tac : (string -> thm) -> int -> tactic
    16.8 +  val exh_tac : Proof.context -> (string -> thm) -> int -> tactic
    16.9  
   16.10    exception Datatype
   16.11    exception Datatype_Empty of string
   16.12 @@ -155,7 +155,7 @@
   16.13  
   16.14  (* perform exhaustive case analysis on last parameter of subgoal i *)
   16.15  
   16.16 -fun exh_tac exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
   16.17 +fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
   16.18    let
   16.19      val thy = Thm.theory_of_cterm cgoal;
   16.20      val goal = term_of cgoal;
   16.21 @@ -167,7 +167,7 @@
   16.22      val exhaustion' =
   16.23        cterm_instantiate [(cterm_of thy (head_of lhs),
   16.24          cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion;
   16.25 -  in compose_tac (false, exhaustion', nprems_of exhaustion) i end);
   16.26 +  in compose_tac ctxt (false, exhaustion', nprems_of exhaustion) i end);
   16.27  
   16.28  
   16.29  (********************** Internal description of datatypes *********************)
    17.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 11:05:20 2014 +0100
    17.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 14:08:00 2014 +0100
    17.3 @@ -431,7 +431,7 @@
    17.4          Goal.prove_sorry_global thy [] [] t
    17.5            (fn {context = ctxt, ...} =>
    17.6              EVERY [resolve_tac [allI] 1,
    17.7 -             Old_Datatype_Aux.exh_tac (K exhaustion) 1,
    17.8 +             Old_Datatype_Aux.exh_tac ctxt (K exhaustion) 1,
    17.9               ALLGOALS (fn i => tac ctxt i (i - 1))])
   17.10        end;
   17.11  
    18.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 09 11:05:20 2014 +0100
    18.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 09 14:08:00 2014 +0100
    18.3 @@ -308,7 +308,7 @@
    18.4            in
    18.5              trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
    18.6                " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
    18.7 -            THEN TRY (Splitter.split_asm_tac [split_asm] 1
    18.8 +            THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
    18.9                THEN (trace_tac ctxt options "after splitting with split_asm rules")
   18.10              (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
   18.11                THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
   18.12 @@ -320,7 +320,7 @@
   18.13        else all_tac
   18.14    in
   18.15      split_term_tac (HOLogic.mk_tuple out_ts)
   18.16 -    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
   18.17 +    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
   18.18      THEN (etac @{thm botE} 2))))
   18.19    end
   18.20  
    19.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Nov 09 11:05:20 2014 +0100
    19.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Nov 09 14:08:00 2014 +0100
    19.3 @@ -392,7 +392,7 @@
    19.4  
    19.5      (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
    19.6      (* merge with previous tactic *)
    19.7 -    Cong_Tac.cong_tac @{thm cong} THEN'
    19.8 +    Cong_Tac.cong_tac ctxt @{thm cong} THEN'
    19.9                   RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
   19.10  
   19.11      (* resolving with R x y assumptions *)
    20.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 11:05:20 2014 +0100
    20.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 14:08:00 2014 +0100
    20.3 @@ -308,14 +308,14 @@
    20.4  
    20.5  (* congruence *)
    20.6  
    20.7 -fun ctac prems i st = st |> (
    20.8 +fun ctac ctxt prems i st = st |> (
    20.9    resolve_tac (@{thm refl} :: prems) i
   20.10 -  ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i))
   20.11 +  ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
   20.12  
   20.13  fun cong_basic ctxt thms t =
   20.14    let val st = Thm.trivial (certify_prop ctxt t)
   20.15    in
   20.16 -    (case Seq.pull (ctac thms 1 st) of
   20.17 +    (case Seq.pull (ctac ctxt thms 1 st) of
   20.18        SOME (thm, _) => thm
   20.19      | NONE => raise THM ("cong", 0, thms @ [st]))
   20.20    end
    21.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Nov 09 11:05:20 2014 +0100
    21.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Nov 09 14:08:00 2014 +0100
    21.3 @@ -723,7 +723,7 @@
    21.4          if null splits orelse length splits > Config.get ctxt split_limit then
    21.5            no_tac
    21.6          else if null (#2 (hd splits)) then
    21.7 -          split_tac split_thms i
    21.8 +          split_tac ctxt split_thms i
    21.9          else
   21.10            (* disallow a split that involves non-locally bound variables      *)
   21.11            (* (except when bound by outermost meta-quantifiers)               *)
   21.12 @@ -866,7 +866,7 @@
   21.13      (* split_limit may trigger.                                           *)
   21.14      (* Therefore splitting outside of simple_tac may allow us to prove    *)
   21.15      (* some goals that simple_tac alone would fail on.                    *)
   21.16 -    (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
   21.17 +    (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
   21.18      (lin_arith_tac ctxt ex);
   21.19  
   21.20  in
    22.1 --- a/src/HOL/Tools/record.ML	Sun Nov 09 11:05:20 2014 +0100
    22.2 +++ b/src/HOL/Tools/record.ML	Sun Nov 09 14:08:00 2014 +0100
    22.3 @@ -1458,7 +1458,7 @@
    22.4    (or on s if there are no parameters).
    22.5    Instatiation of record variable (and predicate) in rule is calculated to
    22.6    avoid problems with higher order unification.*)
    22.7 -fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
    22.8 +fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
    22.9    let
   22.10      val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
   22.11  
   22.12 @@ -1484,7 +1484,7 @@
   22.13            | (_, T) :: _ =>
   22.14                [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
   22.15                  (x, fold_rev Term.abs params (Bound 0))])) rule';
   22.16 -  in compose_tac (false, rule'', nprems_of rule) i end);
   22.17 +  in compose_tac ctxt (false, rule'', nprems_of rule) i end);
   22.18  
   22.19  
   22.20  fun extension_definition name fields alphas zeta moreT more vars thy =
   22.21 @@ -2119,15 +2119,16 @@
   22.22        Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
   22.23          (fn {context = ctxt, ...} =>
   22.24            EVERY
   22.25 -           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
   22.26 -            try_param_tac rN ext_induct 1,
   22.27 +           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt rN ind 1,
   22.28 +            try_param_tac ctxt rN ext_induct 1,
   22.29              asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1]));
   22.30  
   22.31      val induct = timeit_msg ctxt "record induct proof:" (fn () =>
   22.32 -      Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
   22.33 -        try_param_tac rN induct_scheme 1
   22.34 -        THEN try_param_tac "more" @{thm unit.induct} 1
   22.35 -        THEN resolve_tac prems 1));
   22.36 +      Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop)
   22.37 +        (fn {context = ctxt, prems, ...} =>
   22.38 +          try_param_tac ctxt rN induct_scheme 1
   22.39 +          THEN try_param_tac ctxt "more" @{thm unit.induct} 1
   22.40 +          THEN resolve_tac prems 1));
   22.41  
   22.42      val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
   22.43        Goal.prove_sorry_global defs_thy [] [] surjective_prop
   22.44 @@ -2150,7 +2151,7 @@
   22.45      val cases = timeit_msg ctxt "record cases proof:" (fn () =>
   22.46        Goal.prove_sorry_global defs_thy [] [] cases_prop
   22.47          (fn {context = ctxt, ...} =>
   22.48 -          try_param_tac rN cases_scheme 1 THEN
   22.49 +          try_param_tac ctxt rN cases_scheme 1 THEN
   22.50            ALLGOALS (asm_full_simp_tac
   22.51              (put_simpset HOL_basic_ss ctxt addsimps @{thms unit_all_eq1}))));
   22.52  
    23.1 --- a/src/HOL/ex/SVC_Oracle.thy	Sun Nov 09 11:05:20 2014 +0100
    23.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Sun Nov 09 14:08:00 2014 +0100
    23.3 @@ -109,13 +109,15 @@
    23.4    abstracted.  Use via compose_tac, which performs no lifting but will
    23.5    instantiate variables.*)
    23.6  
    23.7 -val svc_tac = CSUBGOAL (fn (ct, i) =>
    23.8 +fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
    23.9    let
   23.10      val thy = Thm.theory_of_cterm ct;
   23.11      val (abs_goal, _) = svc_abstract (Thm.term_of ct);
   23.12      val th = svc_oracle (Thm.cterm_of thy abs_goal);
   23.13 -   in compose_tac (false, th, 0) i end
   23.14 +   in compose_tac ctxt (false, th, 0) i end
   23.15     handle TERM _ => no_tac);
   23.16  *}
   23.17  
   23.18 +method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *}
   23.19 +
   23.20  end
    24.1 --- a/src/HOL/ex/svc_test.thy	Sun Nov 09 11:05:20 2014 +0100
    24.2 +++ b/src/HOL/ex/svc_test.thy	Sun Nov 09 14:08:00 2014 +0100
    24.3 @@ -11,7 +11,7 @@
    24.4    in its length, though @{text "fast"} manages.
    24.5  *}
    24.6  lemma "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P"
    24.7 -  by (tactic {* svc_tac 1 *})
    24.8 +  by svc
    24.9  
   24.10  
   24.11  subsection {* Some big tautologies supplied by John Harrison *}
   24.12 @@ -39,7 +39,7 @@
   24.13     (~v4 | v5 | v6) &
   24.14     (~v7 | ~v8 | v9) &
   24.15     (~v10 | ~v11 | v12))"
   24.16 -  by (tactic {* svc_tac 1 *})
   24.17 +  by svc
   24.18  
   24.19  lemma dk17_be:
   24.20    "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) &
   24.21 @@ -117,7 +117,7 @@
   24.22          (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) &
   24.23          (OUT1 <-> WRES7 & IN8) &
   24.24          (OUT0 <-> WRES7 & ~IN8)"
   24.25 -  by (tactic {* svc_tac 1 *})
   24.26 +  by svc
   24.27  
   24.28  text {* @{text "fast"} only takes a couple of seconds. *}
   24.29  
   24.30 @@ -221,7 +221,7 @@
   24.31          WRES16 & WRES7 |
   24.32          WRES18 & WRES0 & ~IN5 |
   24.33          WRES19)"
   24.34 -  by (tactic {* svc_tac 1 *})
   24.35 +  by svc
   24.36  
   24.37  
   24.38  subsection {* Linear arithmetic *}
   24.39 @@ -229,20 +229,20 @@
   24.40  lemma "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 &
   24.41        x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 &
   24.42        x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"
   24.43 -  by (tactic {* svc_tac 1 *})
   24.44 +  by svc
   24.45  
   24.46  text {*merely to test polarity handling in the presence of biconditionals*}
   24.47  lemma "(x < (y::int)) = (x+1 <= y)"
   24.48 -  by (tactic {* svc_tac 1 *})
   24.49 +  by svc
   24.50  
   24.51  
   24.52  subsection {* Natural number examples requiring implicit "non-negative" assumptions *}
   24.53  
   24.54  lemma "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c &
   24.55        a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c"
   24.56 -  by (tactic {* svc_tac 1 *})
   24.57 +  by svc
   24.58  
   24.59  lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)"
   24.60 -  by (tactic {* svc_tac 1 *})
   24.61 +  by svc
   24.62  
   24.63  end
    25.1 --- a/src/Provers/blast.ML	Sun Nov 09 11:05:20 2014 +0100
    25.2 +++ b/src/Provers/blast.ML	Sun Nov 09 14:08:00 2014 +0100
    25.3 @@ -43,7 +43,7 @@
    25.4    val not_name: string
    25.5    val notE: thm           (* [| ~P;  P |] ==> R *)
    25.6    val ccontr: thm
    25.7 -  val hyp_subst_tac: bool -> int -> tactic
    25.8 +  val hyp_subst_tac: Proof.context -> bool -> int -> tactic
    25.9  end;
   25.10  
   25.11  signature BLAST =
   25.12 @@ -1021,7 +1021,7 @@
   25.13               trace_prover state brs0;
   25.14               if lim<0 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices)
   25.15               else
   25.16 -             prv (Data.hyp_subst_tac trace :: tacs,
   25.17 +             prv (Data.hyp_subst_tac ctxt trace :: tacs,
   25.18                    brs0::trs,  choices,
   25.19                    equalSubst ctxt
   25.20                      (G, {pairs = (br,haz)::pairs,
    26.1 --- a/src/Provers/hypsubst.ML	Sun Nov 09 11:05:20 2014 +0100
    26.2 +++ b/src/Provers/hypsubst.ML	Sun Nov 09 14:08:00 2014 +0100
    26.3 @@ -50,7 +50,7 @@
    26.4    val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
    26.5    val hyp_subst_thin         : bool Config.T
    26.6    val hyp_subst_tac          : Proof.context -> int -> tactic
    26.7 -  val blast_hyp_subst_tac    : bool -> int -> tactic
    26.8 +  val blast_hyp_subst_tac    : Proof.context -> bool -> int -> tactic
    26.9    val stac                   : thm -> int -> tactic
   26.10  end;
   26.11  
   26.12 @@ -162,11 +162,12 @@
   26.13  
   26.14  val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
   26.15  
   26.16 -fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   26.17 +fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) =>
   26.18    case try (Logic.strip_assums_hyp #> hd #>
   26.19        Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   26.20      SOME (t, t') =>
   26.21        let
   26.22 +        val thy = Proof_Context.theory_of ctxt;
   26.23          val Bi = Thm.term_of cBi;
   26.24          val ps = Logic.strip_params Bi;
   26.25          val U = Term.fastype_of1 (rev (map snd ps), t);
   26.26 @@ -182,10 +183,9 @@
   26.27              (case (if b then t else t') of
   26.28                Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   26.29              | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   26.30 -        val thy = Thm.theory_of_thm rl';
   26.31          val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
   26.32        in
   26.33 -        compose_tac (true, Drule.instantiate_normalize (instT,
   26.34 +        compose_tac ctxt (true, Drule.instantiate_normalize (instT,
   26.35            map (pairself (cterm_of thy))
   26.36              [(Var (ixn, Ts ---> U --> body_type T), u),
   26.37               (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   26.38 @@ -204,7 +204,7 @@
   26.39  
   26.40  (*Old version of the tactic above -- slower but the only way
   26.41    to handle equalities containing Vars.*)
   26.42 -fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   26.43 +fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) =>
   26.44        let val n = length(Logic.strip_assums_hyp Bi) - 1
   26.45            val (k, (orient, is_free)) = eq_var bnd false true Bi
   26.46            val rl = if is_free then dup_subst else ssubst
   26.47 @@ -214,7 +214,7 @@
   26.48             (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
   26.49                     rotate_tac 1 i,
   26.50                     REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
   26.51 -                   inst_subst_tac orient rl i,
   26.52 +                   inst_subst_tac ctxt orient rl i,
   26.53                     REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   26.54        end
   26.55        handle THM _ => no_tac | EQ_VAR => no_tac);
   26.56 @@ -224,7 +224,7 @@
   26.57    and on Free variables if thin=true*)
   26.58  fun hyp_subst_tac_thin thin ctxt =
   26.59    REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
   26.60 -    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   26.61 +    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
   26.62      if thin then thin_free_eq_tac else K no_tac];
   26.63  
   26.64  val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
   26.65 @@ -235,7 +235,7 @@
   26.66  (*Substitutes for Bound variables only -- this is always safe*)
   26.67  fun bound_hyp_subst_tac ctxt =
   26.68    REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   26.69 -    ORELSE' vars_gen_hyp_subst_tac true);
   26.70 +    ORELSE' vars_gen_hyp_subst_tac ctxt true);
   26.71  
   26.72  (** Version for Blast_tac.  Hyps that are affected by the substitution are
   26.73      moved to the front.  Defect: even trivial changes are noticed, such as
   26.74 @@ -270,7 +270,7 @@
   26.75    in imptac (0, rev hyps) end;
   26.76  
   26.77  
   26.78 -fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   26.79 +fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi,i) =>
   26.80        let val (k, (symopt, _)) = eq_var false false false Bi
   26.81            val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   26.82            (*omit selected equality, returning other hyps*)
   26.83 @@ -282,7 +282,7 @@
   26.84             (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
   26.85                     rotate_tac 1 i,
   26.86                     REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
   26.87 -                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   26.88 +                   inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
   26.89                     all_imp_intr_tac hyps i])
   26.90        end
   26.91        handle THM _ => no_tac | EQ_VAR => no_tac);
    27.1 --- a/src/Provers/splitter.ML	Sun Nov 09 11:05:20 2014 +0100
    27.2 +++ b/src/Provers/splitter.ML	Sun Nov 09 14:08:00 2014 +0100
    27.3 @@ -29,9 +29,9 @@
    27.4      theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list
    27.5      (* first argument is a "cmap", returns a list of "split packs" *)
    27.6    (* the "real" interface, providing a number of tactics *)
    27.7 -  val split_tac       : thm list -> int -> tactic
    27.8 -  val split_inside_tac: thm list -> int -> tactic
    27.9 -  val split_asm_tac   : thm list -> int -> tactic
   27.10 +  val split_tac       : Proof.context -> thm list -> int -> tactic
   27.11 +  val split_inside_tac: Proof.context -> thm list -> int -> tactic
   27.12 +  val split_asm_tac   : Proof.context -> thm list -> int -> tactic
   27.13    val add_split: thm -> Proof.context -> Proof.context
   27.14    val del_split: thm -> Proof.context -> Proof.context
   27.15    val split_add: attribute
   27.16 @@ -353,17 +353,17 @@
   27.17     i      : number of subgoal the tactic should be applied to
   27.18  *****************************************************************************)
   27.19  
   27.20 -fun split_tac [] i = no_tac
   27.21 -  | split_tac splits i =
   27.22 +fun split_tac _ [] i = no_tac
   27.23 +  | split_tac ctxt splits i =
   27.24    let val cmap = cmap_of_split_thms splits
   27.25 -      fun lift_tac Ts t p st = compose_tac (false, inst_lift Ts t p st i, 2) i st
   27.26 +      fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st
   27.27        fun lift_split_tac state =
   27.28              let val (Ts, t, splits) = select cmap state i
   27.29              in case splits of
   27.30                   [] => no_tac state
   27.31                 | (thm, apsns, pos, TB, tt)::_ =>
   27.32                     (case apsns of
   27.33 -                      [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
   27.34 +                      [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state
   27.35                      | p::_ => EVERY [lift_tac Ts t p,
   27.36                                       resolve_tac [reflexive_thm] (i+1),
   27.37                                       lift_split_tac] state)
   27.38 @@ -385,8 +385,8 @@
   27.39  
   27.40     splits : list of split-theorems to be tried
   27.41  ****************************************************************************)
   27.42 -fun split_asm_tac [] = K no_tac
   27.43 -  | split_asm_tac splits =
   27.44 +fun split_asm_tac _ [] = K no_tac
   27.45 +  | split_asm_tac ctxt splits =
   27.46  
   27.47    let val cname_list = map (fst o fst o split_thm_info) splits;
   27.48        fun tac (t,i) =
   27.49 @@ -408,18 +408,18 @@
   27.50                             THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
   27.51            in if n<0 then  no_tac  else (DETERM (EVERY'
   27.52                  [rotate_tac n, eresolve_tac [Data.contrapos2],
   27.53 -                 split_tac splits,
   27.54 +                 split_tac ctxt splits,
   27.55                   rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
   27.56                   flat_prems_tac] i))
   27.57            end;
   27.58    in SUBGOAL tac
   27.59    end;
   27.60  
   27.61 -fun gen_split_tac [] = K no_tac
   27.62 -  | gen_split_tac (split::splits) =
   27.63 +fun gen_split_tac _ [] = K no_tac
   27.64 +  | gen_split_tac ctxt (split::splits) =
   27.65        let val (_,asm) = split_thm_info split
   27.66 -      in (if asm then split_asm_tac else split_tac) [split] ORELSE'
   27.67 -         gen_split_tac splits
   27.68 +      in (if asm then split_asm_tac else split_tac) ctxt [split] ORELSE'
   27.69 +         gen_split_tac ctxt splits
   27.70        end;
   27.71  
   27.72  
   27.73 @@ -437,8 +437,8 @@
   27.74  fun add_split split ctxt =
   27.75    let
   27.76      val (name, asm) = split_thm_info split
   27.77 -    val tac = (if asm then split_asm_tac else split_tac) [split]
   27.78 -  in Simplifier.addloop (ctxt, (split_name name asm, K tac)) end;
   27.79 +    fun tac ctxt' = (if asm then split_asm_tac else split_tac) ctxt' [split]
   27.80 +  in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
   27.81  
   27.82  fun del_split split ctxt =
   27.83    let val (name, asm) = split_thm_info split
   27.84 @@ -468,7 +468,7 @@
   27.85  val _ =
   27.86    Theory.setup
   27.87      (Method.setup @{binding split}
   27.88 -      (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
   27.89 +      (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ctxt ths)))
   27.90        "apply case split rule");
   27.91  
   27.92  end;
    28.1 --- a/src/Pure/Isar/expression.ML	Sun Nov 09 11:05:20 2014 +0100
    28.2 +++ b/src/Pure/Isar/expression.ML	Sun Nov 09 14:08:00 2014 +0100
    28.3 @@ -683,8 +683,9 @@
    28.4      val intro = Goal.prove_global defs_thy [] norm_ts statement
    28.5        (fn {context = ctxt, ...} =>
    28.6          rewrite_goals_tac ctxt [pred_def] THEN
    28.7 -        compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    28.8 -        compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    28.9 +        compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   28.10 +        compose_tac defs_ctxt
   28.11 +          (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   28.12  
   28.13      val conjuncts =
   28.14        (Drule.equal_elim_rule2 OF
   28.15 @@ -695,7 +696,7 @@
   28.16        |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
   28.17      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   28.18        Element.prove_witness axioms_ctxt t
   28.19 -       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
   28.20 +       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
   28.21    in ((statement, intro, axioms), defs_thy) end;
   28.22  
   28.23  in
    29.1 --- a/src/Pure/Tools/rule_insts.ML	Sun Nov 09 11:05:20 2014 +0100
    29.2 +++ b/src/Pure/Tools/rule_insts.ML	Sun Nov 09 14:08:00 2014 +0100
    29.3 @@ -270,7 +270,7 @@
    29.4                (map lifttvar envT', map liftpair cenv)
    29.5                (Thm.lift_rule cgoal thm)
    29.6        in
    29.7 -        compose_tac (bires_flag, rule, nprems_of thm) i
    29.8 +        compose_tac ctxt' (bires_flag, rule, nprems_of thm) i
    29.9        end) i st;
   29.10    in tac end;
   29.11  
    30.1 --- a/src/Pure/tactic.ML	Sun Nov 09 11:05:20 2014 +0100
    30.2 +++ b/src/Pure/tactic.ML	Sun Nov 09 14:08:00 2014 +0100
    30.3 @@ -10,7 +10,7 @@
    30.4    val rule_by_tactic: Proof.context -> tactic -> thm -> thm
    30.5    val assume_tac: int -> tactic
    30.6    val eq_assume_tac: int -> tactic
    30.7 -  val compose_tac: (bool * thm * int) -> int -> tactic
    30.8 +  val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic
    30.9    val make_elim: thm -> thm
   30.10    val biresolve_tac: (bool * thm) list -> int -> tactic
   30.11    val resolve_tac: thm list -> int -> tactic
   30.12 @@ -111,8 +111,8 @@
   30.13  
   30.14  (*The composition rule/state: no lifting or var renaming.
   30.15    The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
   30.16 -fun compose_tac arg i =
   30.17 -  PRIMSEQ (Thm.bicompose NONE {flatten = true, match = false, incremented = false} arg i);
   30.18 +fun compose_tac ctxt arg i =
   30.19 +  PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} arg i);
   30.20  
   30.21  (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   30.22    like [| P&Q; P==>R |] ==> R *)
    31.1 --- a/src/Tools/atomize_elim.ML	Sun Nov 09 11:05:20 2014 +0100
    31.2 +++ b/src/Tools/atomize_elim.ML	Sun Nov 09 14:08:00 2014 +0100
    31.3 @@ -120,7 +120,7 @@
    31.4                val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
    31.5                           @{thm meta_spec}
    31.6              in
    31.7 -              compose_tac (false, rule, 1) i
    31.8 +              compose_tac ctxt (false, rule, 1) i
    31.9              end
   31.10      in
   31.11        quantify_thesis
    32.1 --- a/src/Tools/cong_tac.ML	Sun Nov 09 11:05:20 2014 +0100
    32.2 +++ b/src/Tools/cong_tac.ML	Sun Nov 09 14:08:00 2014 +0100
    32.3 @@ -6,13 +6,13 @@
    32.4  
    32.5  signature CONG_TAC =
    32.6  sig
    32.7 -  val cong_tac: thm -> int -> tactic
    32.8 +  val cong_tac: Proof.context -> thm -> int -> tactic
    32.9  end;
   32.10  
   32.11  structure Cong_Tac: CONG_TAC =
   32.12  struct
   32.13  
   32.14 -fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
   32.15 +fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
   32.16    let
   32.17      val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
   32.18      val goal = Thm.term_of cgoal;
   32.19 @@ -28,7 +28,7 @@
   32.20              |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
   32.21          in
   32.22            fn st =>
   32.23 -            compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
   32.24 +            compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
   32.25                handle THM _ => no_tac st
   32.26          end
   32.27      | _ => no_tac)
    33.1 --- a/src/Tools/induct.ML	Sun Nov 09 11:05:20 2014 +0100
    33.2 +++ b/src/Tools/induct.ML	Sun Nov 09 14:08:00 2014 +0100
    33.3 @@ -684,7 +684,7 @@
    33.4    in
    33.5      (case goal_concl n [] goal of
    33.6        SOME concl =>
    33.7 -        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
    33.8 +        (compose_tac ctxt (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
    33.9            resolve_tac [asm_rl]) i
   33.10      | NONE => all_tac)
   33.11    end);