# HG changeset patch
# User wenzelm
# Date 1415538480 -3600
# Node ID a816aa3ff391152e714a2774729ee29b99ab8f62
# Parent  1694bad185684e161cfdc1a03b3450d8d7ea2df5
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

diff -r 1694bad18568 -r a816aa3ff391 NEWS
--- a/NEWS	Sun Nov 09 11:05:20 2014 +0100
+++ b/NEWS	Sun Nov 09 14:08:00 2014 +0100
@@ -190,6 +190,9 @@
 
 *** ML ***
 
+* Proper context for various elementary tactics: compose_tac,
+Splitter.split_tac etc.  Minor INCOMPATIBILITY.
+
 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
 PARALLEL_GOALS.
 
diff -r 1694bad18568 -r a816aa3ff391 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Doc/Implementation/Tactic.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -492,14 +492,14 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
+  @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
   @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
   @{index_ML_op COMP: "thm * thm -> thm"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML compose_tac}~@{text "(flag, rule, m) i"} refines subgoal
+  \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
   @{text "i"} using @{text "rule"}, without lifting.  The @{text
   "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
   @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -47,7 +47,7 @@
 
 fun linr_tac ctxt q =
     Object_Logic.atomize_prems_tac ctxt
-        THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
+        THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
         THEN' SUBGOAL (fn (g, i) =>
   let
     val thy = Proof_Context.theory_of ctxt
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -67,7 +67,7 @@
     Object_Logic.atomize_prems_tac ctxt
         THEN' simp_tac (put_simpset HOL_basic_ss ctxt
           addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
-        THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
+        THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
         THEN' SUBGOAL (fn (g, i) =>
   let
     val thy = Proof_Context.theory_of ctxt
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/HOL.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -274,7 +274,7 @@
 apply (rule refl)
 done
 
-ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
+ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *}
 
 
 subsubsection {* Equality of booleans -- iff *}
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/HOLCF/Tr.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -154,7 +154,7 @@
 ML {*
 fun split_If_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
-    THEN' (split_tac [@{thm split_If2}])
+    THEN' (split_tac ctxt [@{thm split_If2}])
 *}
 
 subsection "Rewriting of HOLCF operations to HOL functions"
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -88,7 +88,7 @@
 
 fun tac ctxt {splits, intros, defs} =
   let val ctxt' = Classical.addSIs (ctxt, intros) in
-    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
+    REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt splits))
     THEN Local_Defs.unfold_tac ctxt defs
     THEN safe_tac ctxt'
   end
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/List.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -610,7 +610,7 @@
       | dest_if _ = NONE
     fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
       | tac ctxt (If :: cont) =
-          Splitter.split_tac [@{thm split_if}] 1
+          Splitter.split_tac ctxt [@{thm split_if}] 1
           THEN rtac @{thm conjI} 1
           THEN rtac @{thm impI} 1
           THEN Subgoal.FOCUS (fn {prems, context, ...} =>
@@ -631,7 +631,7 @@
               Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
           in
             (* do case distinction *)
-            Splitter.split_tac [split] 1
+            Splitter.split_tac ctxt [split] 1
             THEN EVERY (map_index (fn (i', _) =>
               (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
               THEN REPEAT_DETERM (rtac @{thm allI} 1)
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -654,7 +654,7 @@
                 ((Rep RS perm_closed1 RS Abs_inverse) ::
                  (if atom1 = atom2 then []
                   else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
-              cong_tac 1,
+              cong_tac ctxt 1,
               rtac refl 1,
               rtac cp1' 1]) thy)
         (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -10,7 +10,7 @@
 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
 
 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
-fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
+fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
   let
     val thy = theory_of_thm st;
     val cgoal = nth (cprems_of st) (i - 1);
@@ -27,18 +27,18 @@
       (map (pairself (cterm_of thy)) tinst')
       (Thm.lift_rule cgoal th)
   in
-    compose_tac (elim, th', nprems_of th) i st
+    compose_tac ctxt (elim, th', nprems_of th) i st
   end handle General.Subscript => Seq.empty;
 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
 
-val res_inst_tac_term =
-  gen_res_inst_tac_term (curry Thm.instantiate);
+fun res_inst_tac_term ctxt =
+  gen_res_inst_tac_term ctxt (curry Thm.instantiate);
 
-val res_inst_tac_term' =
-  gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
+fun res_inst_tac_term' ctxt =
+  gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) [];
 
 fun cut_inst_tac_term' ctxt tinst th =
-  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th);
+  res_inst_tac_term' ctxt tinst false (Rule_Insts.make_elim_preserve ctxt th);
 
 fun get_dyn_thm thy name atom_name =
   Global_Theory.get_thm thy name handle ERROR _ =>
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -227,7 +227,7 @@
       asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
       asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
 
-fun apply_cong_tac i = ("application of congruence", cong_tac i);
+fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
 
 
 (* unfolds the definition of permutations     *)
@@ -256,7 +256,7 @@
                (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i),
                        fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
                        fn i => tactical ctxt (perm_compose_tac ctxt i),
-                       fn i => tactical ctxt (apply_cong_tac i), 
+                       fn i => tactical ctxt (apply_cong_tac ctxt i), 
                        fn i => tactical ctxt (unfold_perm_fun_def_tac i),
                        fn i => tactical ctxt (ext_fun_tac i)]
                       THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
@@ -315,7 +315,7 @@
             val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
           in
             (tactical ctxt ("guessing of the right supports-set",
-                      EVERY [compose_tac (false, supports_rule'', 2) i,
+                      EVERY [compose_tac ctxt (false, supports_rule'', 2) i,
                              asm_full_simp_tac ctxt' (i+1),
                              supports_tac_i tactical ctxt i])) st
           end
@@ -357,7 +357,7 @@
               [(cert (head_of S), cert s')] supports_fresh_rule'
           in
             (tactical ctxt ("guessing of the right set that supports the goal", 
-                      (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
+                      (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
                              asm_full_simp_tac ctxt1 (i+2),
                              asm_full_simp_tac ctxt2 (i+1), 
                              supports_tac_i tactical ctxt i]))) st
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -376,7 +376,7 @@
     Proof.apply (Method.Basic (fn ctxt => fn _ =>
       NO_CASES
        (rewrite_goals_tac ctxt defs_thms THEN
-        compose_tac (false, rule, length rule_prems) 1))) |>
+        compose_tac ctxt (false, rule, length rule_prems) 1))) |>
     Seq.hd
   end;
 
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -209,7 +209,7 @@
       (fn _ =>
          rtac @{thm subset_antisym} 1 THEN
          rtac @{thm subsetI} 1 THEN
-         Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
+         Old_Datatype_Aux.exh_tac lthy (K (#exhaust (BNF_LFP_Compat.the_info
            (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
          ALLGOALS (asm_full_simp_tac lthy));
 
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -133,8 +133,8 @@
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
     eresolve_tac falseEs ORELSE'
     resolve_tac split_connectI ORELSE'
-    Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
-    Splitter.split_tac (split_if :: splits) ORELSE'
+    Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
+    Splitter.split_tac ctxt (split_if :: splits) ORELSE'
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
@@ -171,8 +171,8 @@
       SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
       (rtac refl ORELSE' atac ORELSE'
        resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
-       Splitter.split_tac (split_if :: splits) ORELSE'
-       Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
+       Splitter.split_tac ctxt (split_if :: splits) ORELSE'
+       Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
        mk_primcorec_assumption_tac ctxt discIs ORELSE'
        distinct_in_prems_tac distincts ORELSE'
        (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
@@ -204,7 +204,7 @@
     SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
     (rtac refl ORELSE' atac ORELSE'
      resolve_tac split_connectI ORELSE'
-     Splitter.split_tac (split_if :: splits) ORELSE'
+     Splitter.split_tac ctxt (split_if :: splits) ORELSE'
      distinct_in_prems_tac distincts ORELSE'
      rtac sym THEN' atac ORELSE'
      etac notE THEN' atac));
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -421,7 +421,7 @@
               [(Old_Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
                REPEAT (EVERY
                  [rtac allI 1, rtac impI 1,
-                  Old_Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
+                  Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1,
                   REPEAT (EVERY
                     [hyp_subst_tac ctxt 1,
                      rewrite_goals_tac ctxt rewrites,
@@ -430,7 +430,7 @@
                      ORELSE (EVERY
                        [REPEAT (eresolve_tac (Scons_inject ::
                           map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
-                        REPEAT (cong_tac 1), rtac refl 1,
+                        REPEAT (cong_tac ctxt 1), rtac refl 1,
                         REPEAT (atac 1 ORELSE (EVERY
                           [REPEAT (rtac @{thm ext} 1),
                            REPEAT (eresolve_tac (mp :: allE ::
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -53,7 +53,7 @@
   val app_bnds : term -> int -> term
 
   val ind_tac : thm -> string list -> int -> tactic
-  val exh_tac : (string -> thm) -> int -> tactic
+  val exh_tac : Proof.context -> (string -> thm) -> int -> tactic
 
   exception Datatype
   exception Datatype_Empty of string
@@ -155,7 +155,7 @@
 
 (* perform exhaustive case analysis on last parameter of subgoal i *)
 
-fun exh_tac exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
+fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
   let
     val thy = Thm.theory_of_cterm cgoal;
     val goal = term_of cgoal;
@@ -167,7 +167,7 @@
     val exhaustion' =
       cterm_instantiate [(cterm_of thy (head_of lhs),
         cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion;
-  in compose_tac (false, exhaustion', nprems_of exhaustion) i end);
+  in compose_tac ctxt (false, exhaustion', nprems_of exhaustion) i end);
 
 
 (********************** Internal description of datatypes *********************)
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -431,7 +431,7 @@
         Goal.prove_sorry_global thy [] [] t
           (fn {context = ctxt, ...} =>
             EVERY [resolve_tac [allI] 1,
-             Old_Datatype_Aux.exh_tac (K exhaustion) 1,
+             Old_Datatype_Aux.exh_tac ctxt (K exhaustion) 1,
              ALLGOALS (fn i => tac ctxt i (i - 1))])
       end;
 
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -308,7 +308,7 @@
           in
             trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
               " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
-            THEN TRY (Splitter.split_asm_tac [split_asm] 1
+            THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
               THEN (trace_tac ctxt options "after splitting with split_asm rules")
             (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
               THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
@@ -320,7 +320,7 @@
       else all_tac
   in
     split_term_tac (HOLogic.mk_tuple out_ts)
-    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
+    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
     THEN (etac @{thm botE} 2))))
   end
 
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -392,7 +392,7 @@
 
     (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
-    Cong_Tac.cong_tac @{thm cong} THEN'
+    Cong_Tac.cong_tac ctxt @{thm cong} THEN'
                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
 
     (* resolving with R x y assumptions *)
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -308,14 +308,14 @@
 
 (* congruence *)
 
-fun ctac prems i st = st |> (
+fun ctac ctxt prems i st = st |> (
   resolve_tac (@{thm refl} :: prems) i
-  ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i))
+  ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
 
 fun cong_basic ctxt thms t =
   let val st = Thm.trivial (certify_prop ctxt t)
   in
-    (case Seq.pull (ctac thms 1 st) of
+    (case Seq.pull (ctac ctxt thms 1 st) of
       SOME (thm, _) => thm
     | NONE => raise THM ("cong", 0, thms @ [st]))
   end
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -723,7 +723,7 @@
         if null splits orelse length splits > Config.get ctxt split_limit then
           no_tac
         else if null (#2 (hd splits)) then
-          split_tac split_thms i
+          split_tac ctxt split_thms i
         else
           (* disallow a split that involves non-locally bound variables      *)
           (* (except when bound by outermost meta-quantifiers)               *)
@@ -866,7 +866,7 @@
     (* split_limit may trigger.                                           *)
     (* Therefore splitting outside of simple_tac may allow us to prove    *)
     (* some goals that simple_tac alone would fail on.                    *)
-    (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
+    (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
     (lin_arith_tac ctxt ex);
 
 in
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/record.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -1458,7 +1458,7 @@
   (or on s if there are no parameters).
   Instatiation of record variable (and predicate) in rule is calculated to
   avoid problems with higher order unification.*)
-fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
+fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
   let
     val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
 
@@ -1484,7 +1484,7 @@
           | (_, T) :: _ =>
               [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
                 (x, fold_rev Term.abs params (Bound 0))])) rule';
-  in compose_tac (false, rule'', nprems_of rule) i end);
+  in compose_tac ctxt (false, rule'', nprems_of rule) i end);
 
 
 fun extension_definition name fields alphas zeta moreT more vars thy =
@@ -2119,15 +2119,16 @@
       Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
         (fn {context = ctxt, ...} =>
           EVERY
-           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
-            try_param_tac rN ext_induct 1,
+           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt rN ind 1,
+            try_param_tac ctxt rN ext_induct 1,
             asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1]));
 
     val induct = timeit_msg ctxt "record induct proof:" (fn () =>
-      Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
-        try_param_tac rN induct_scheme 1
-        THEN try_param_tac "more" @{thm unit.induct} 1
-        THEN resolve_tac prems 1));
+      Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop)
+        (fn {context = ctxt, prems, ...} =>
+          try_param_tac ctxt rN induct_scheme 1
+          THEN try_param_tac ctxt "more" @{thm unit.induct} 1
+          THEN resolve_tac prems 1));
 
     val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] surjective_prop
@@ -2150,7 +2151,7 @@
     val cases = timeit_msg ctxt "record cases proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] cases_prop
         (fn {context = ctxt, ...} =>
-          try_param_tac rN cases_scheme 1 THEN
+          try_param_tac ctxt rN cases_scheme 1 THEN
           ALLGOALS (asm_full_simp_tac
             (put_simpset HOL_basic_ss ctxt addsimps @{thms unit_all_eq1}))));
 
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -109,13 +109,15 @@
   abstracted.  Use via compose_tac, which performs no lifting but will
   instantiate variables.*)
 
-val svc_tac = CSUBGOAL (fn (ct, i) =>
+fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
   let
     val thy = Thm.theory_of_cterm ct;
     val (abs_goal, _) = svc_abstract (Thm.term_of ct);
     val th = svc_oracle (Thm.cterm_of thy abs_goal);
-   in compose_tac (false, th, 0) i end
+   in compose_tac ctxt (false, th, 0) i end
    handle TERM _ => no_tac);
 *}
 
+method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *}
+
 end
diff -r 1694bad18568 -r a816aa3ff391 src/HOL/ex/svc_test.thy
--- a/src/HOL/ex/svc_test.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/ex/svc_test.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -11,7 +11,7 @@
   in its length, though @{text "fast"} manages.
 *}
 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"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 
 subsection {* Some big tautologies supplied by John Harrison *}
@@ -39,7 +39,7 @@
    (~v4 | v5 | v6) &
    (~v7 | ~v8 | v9) &
    (~v10 | ~v11 | v12))"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 lemma dk17_be:
   "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) &
@@ -117,7 +117,7 @@
         (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) &
         (OUT1 <-> WRES7 & IN8) &
         (OUT0 <-> WRES7 & ~IN8)"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 text {* @{text "fast"} only takes a couple of seconds. *}
 
@@ -221,7 +221,7 @@
         WRES16 & WRES7 |
         WRES18 & WRES0 & ~IN5 |
         WRES19)"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 
 subsection {* Linear arithmetic *}
@@ -229,20 +229,20 @@
 lemma "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 &
       x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 &
       x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 text {*merely to test polarity handling in the presence of biconditionals*}
 lemma "(x < (y::int)) = (x+1 <= y)"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 
 subsection {* Natural number examples requiring implicit "non-negative" assumptions *}
 
 lemma "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c &
       a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)"
-  by (tactic {* svc_tac 1 *})
+  by svc
 
 end
diff -r 1694bad18568 -r a816aa3ff391 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Provers/blast.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -43,7 +43,7 @@
   val not_name: string
   val notE: thm           (* [| ~P;  P |] ==> R *)
   val ccontr: thm
-  val hyp_subst_tac: bool -> int -> tactic
+  val hyp_subst_tac: Proof.context -> bool -> int -> tactic
 end;
 
 signature BLAST =
@@ -1021,7 +1021,7 @@
              trace_prover state brs0;
              if lim<0 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices)
              else
-             prv (Data.hyp_subst_tac trace :: tacs,
+             prv (Data.hyp_subst_tac ctxt trace :: tacs,
                   brs0::trs,  choices,
                   equalSubst ctxt
                     (G, {pairs = (br,haz)::pairs,
diff -r 1694bad18568 -r a816aa3ff391 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Provers/hypsubst.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -50,7 +50,7 @@
   val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
   val hyp_subst_thin         : bool Config.T
   val hyp_subst_tac          : Proof.context -> int -> tactic
-  val blast_hyp_subst_tac    : bool -> int -> tactic
+  val blast_hyp_subst_tac    : Proof.context -> bool -> int -> tactic
   val stac                   : thm -> int -> tactic
 end;
 
@@ -162,11 +162,12 @@
 
 val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
 
-fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
+fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) =>
   case try (Logic.strip_assums_hyp #> hd #>
       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
     SOME (t, t') =>
       let
+        val thy = Proof_Context.theory_of ctxt;
         val Bi = Thm.term_of cBi;
         val ps = Logic.strip_params Bi;
         val U = Term.fastype_of1 (rev (map snd ps), t);
@@ -182,10 +183,9 @@
             (case (if b then t else t') of
               Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
             | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
-        val thy = Thm.theory_of_thm rl';
         val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
       in
-        compose_tac (true, Drule.instantiate_normalize (instT,
+        compose_tac ctxt (true, Drule.instantiate_normalize (instT,
           map (pairself (cterm_of thy))
             [(Var (ixn, Ts ---> U --> body_type T), u),
              (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
@@ -204,7 +204,7 @@
 
 (*Old version of the tactic above -- slower but the only way
   to handle equalities containing Vars.*)
-fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
+fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) =>
       let val n = length(Logic.strip_assums_hyp Bi) - 1
           val (k, (orient, is_free)) = eq_var bnd false true Bi
           val rl = if is_free then dup_subst else ssubst
@@ -214,7 +214,7 @@
            (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
                    rotate_tac 1 i,
                    REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
-                   inst_subst_tac orient rl i,
+                   inst_subst_tac ctxt orient rl i,
                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
       end
       handle THM _ => no_tac | EQ_VAR => no_tac);
@@ -224,7 +224,7 @@
   and on Free variables if thin=true*)
 fun hyp_subst_tac_thin thin ctxt =
   REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
-    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
+    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
     if thin then thin_free_eq_tac else K no_tac];
 
 val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
@@ -235,7 +235,7 @@
 (*Substitutes for Bound variables only -- this is always safe*)
 fun bound_hyp_subst_tac ctxt =
   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
-    ORELSE' vars_gen_hyp_subst_tac true);
+    ORELSE' vars_gen_hyp_subst_tac ctxt true);
 
 (** Version for Blast_tac.  Hyps that are affected by the substitution are
     moved to the front.  Defect: even trivial changes are noticed, such as
@@ -270,7 +270,7 @@
   in imptac (0, rev hyps) end;
 
 
-fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
+fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi,i) =>
       let val (k, (symopt, _)) = eq_var false false false Bi
           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
           (*omit selected equality, returning other hyps*)
@@ -282,7 +282,7 @@
            (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
                    rotate_tac 1 i,
                    REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
-                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
+                   inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
                    all_imp_intr_tac hyps i])
       end
       handle THM _ => no_tac | EQ_VAR => no_tac);
diff -r 1694bad18568 -r a816aa3ff391 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Provers/splitter.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -29,9 +29,9 @@
     theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list
     (* first argument is a "cmap", returns a list of "split packs" *)
   (* the "real" interface, providing a number of tactics *)
-  val split_tac       : thm list -> int -> tactic
-  val split_inside_tac: thm list -> int -> tactic
-  val split_asm_tac   : thm list -> int -> tactic
+  val split_tac       : Proof.context -> thm list -> int -> tactic
+  val split_inside_tac: Proof.context -> thm list -> int -> tactic
+  val split_asm_tac   : Proof.context -> thm list -> int -> tactic
   val add_split: thm -> Proof.context -> Proof.context
   val del_split: thm -> Proof.context -> Proof.context
   val split_add: attribute
@@ -353,17 +353,17 @@
    i      : number of subgoal the tactic should be applied to
 *****************************************************************************)
 
-fun split_tac [] i = no_tac
-  | split_tac splits i =
+fun split_tac _ [] i = no_tac
+  | split_tac ctxt splits i =
   let val cmap = cmap_of_split_thms splits
-      fun lift_tac Ts t p st = compose_tac (false, inst_lift Ts t p st i, 2) i st
+      fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st
       fun lift_split_tac state =
             let val (Ts, t, splits) = select cmap state i
             in case splits of
                  [] => no_tac state
                | (thm, apsns, pos, TB, tt)::_ =>
                    (case apsns of
-                      [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
+                      [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state
                     | p::_ => EVERY [lift_tac Ts t p,
                                      resolve_tac [reflexive_thm] (i+1),
                                      lift_split_tac] state)
@@ -385,8 +385,8 @@
 
    splits : list of split-theorems to be tried
 ****************************************************************************)
-fun split_asm_tac [] = K no_tac
-  | split_asm_tac splits =
+fun split_asm_tac _ [] = K no_tac
+  | split_asm_tac ctxt splits =
 
   let val cname_list = map (fst o fst o split_thm_info) splits;
       fun tac (t,i) =
@@ -408,18 +408,18 @@
                            THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
           in if n<0 then  no_tac  else (DETERM (EVERY'
                 [rotate_tac n, eresolve_tac [Data.contrapos2],
-                 split_tac splits,
+                 split_tac ctxt splits,
                  rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
                  flat_prems_tac] i))
           end;
   in SUBGOAL tac
   end;
 
-fun gen_split_tac [] = K no_tac
-  | gen_split_tac (split::splits) =
+fun gen_split_tac _ [] = K no_tac
+  | gen_split_tac ctxt (split::splits) =
       let val (_,asm) = split_thm_info split
-      in (if asm then split_asm_tac else split_tac) [split] ORELSE'
-         gen_split_tac splits
+      in (if asm then split_asm_tac else split_tac) ctxt [split] ORELSE'
+         gen_split_tac ctxt splits
       end;
 
 
@@ -437,8 +437,8 @@
 fun add_split split ctxt =
   let
     val (name, asm) = split_thm_info split
-    val tac = (if asm then split_asm_tac else split_tac) [split]
-  in Simplifier.addloop (ctxt, (split_name name asm, K tac)) end;
+    fun tac ctxt' = (if asm then split_asm_tac else split_tac) ctxt' [split]
+  in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
 
 fun del_split split ctxt =
   let val (name, asm) = split_thm_info split
@@ -468,7 +468,7 @@
 val _ =
   Theory.setup
     (Method.setup @{binding split}
-      (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+      (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ctxt ths)))
       "apply case split rule");
 
 end;
diff -r 1694bad18568 -r a816aa3ff391 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -683,8 +683,9 @@
     val intro = Goal.prove_global defs_thy [] norm_ts statement
       (fn {context = ctxt, ...} =>
         rewrite_goals_tac ctxt [pred_def] THEN
-        compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
-        compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+        compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+        compose_tac defs_ctxt
+          (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF
@@ -695,7 +696,7 @@
       |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness axioms_ctxt t
-       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
+       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 in
diff -r 1694bad18568 -r a816aa3ff391 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -270,7 +270,7 @@
               (map lifttvar envT', map liftpair cenv)
               (Thm.lift_rule cgoal thm)
       in
-        compose_tac (bires_flag, rule, nprems_of thm) i
+        compose_tac ctxt' (bires_flag, rule, nprems_of thm) i
       end) i st;
   in tac end;
 
diff -r 1694bad18568 -r a816aa3ff391 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Pure/tactic.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -10,7 +10,7 @@
   val rule_by_tactic: Proof.context -> tactic -> thm -> thm
   val assume_tac: int -> tactic
   val eq_assume_tac: int -> tactic
-  val compose_tac: (bool * thm * int) -> int -> tactic
+  val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic
   val make_elim: thm -> thm
   val biresolve_tac: (bool * thm) list -> int -> tactic
   val resolve_tac: thm list -> int -> tactic
@@ -111,8 +111,8 @@
 
 (*The composition rule/state: no lifting or var renaming.
   The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
-fun compose_tac arg i =
-  PRIMSEQ (Thm.bicompose NONE {flatten = true, match = false, incremented = false} arg i);
+fun compose_tac ctxt arg i =
+  PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} arg i);
 
 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   like [| P&Q; P==>R |] ==> R *)
diff -r 1694bad18568 -r a816aa3ff391 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/atomize_elim.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -120,7 +120,7 @@
               val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
                          @{thm meta_spec}
             in
-              compose_tac (false, rule, 1) i
+              compose_tac ctxt (false, rule, 1) i
             end
     in
       quantify_thesis
diff -r 1694bad18568 -r a816aa3ff391 src/Tools/cong_tac.ML
--- a/src/Tools/cong_tac.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/cong_tac.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -6,13 +6,13 @@
 
 signature CONG_TAC =
 sig
-  val cong_tac: thm -> int -> tactic
+  val cong_tac: Proof.context -> thm -> int -> tactic
 end;
 
 structure Cong_Tac: CONG_TAC =
 struct
 
-fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
+fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
   let
     val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
     val goal = Thm.term_of cgoal;
@@ -28,7 +28,7 @@
             |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
         in
           fn st =>
-            compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+            compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
               handle THM _ => no_tac st
         end
     | _ => no_tac)
diff -r 1694bad18568 -r a816aa3ff391 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/induct.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -684,7 +684,7 @@
   in
     (case goal_concl n [] goal of
       SOME concl =>
-        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
+        (compose_tac ctxt (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
           resolve_tac [asm_rl]) i
     | NONE => all_tac)
   end);