# HG changeset patch
# User wenzelm
# Date 1423867165 -3600
# Node ID c3ca292c1484dac36a600fa8e1306a7bfc2a283b
# Parent  4862f3dc954081b870fab14113de6075b46c9303# Parent  e9ffe89a20a483877f3a6bfed7b37a7797ca3e01
merged

diff -r 4862f3dc9540 -r c3ca292c1484 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/FOL/IFOL.thy	Fri Feb 13 23:39:25 2015 +0100
@@ -208,8 +208,8 @@
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
 ML {*
-  fun mp_tac i = eresolve0_tac [@{thm notE}, @{thm impE}] i  THEN  atac i
-  fun eq_mp_tac i = eresolve0_tac [@{thm notE}, @{thm impE}] i  THEN  eq_assume_tac i
+  fun mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i
+  fun eq_mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i
 *}
 
 
@@ -304,18 +304,20 @@
 
 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
 ML {*
-  fun iff_tac prems i =
-    resolve0_tac (prems RL @{thms iffE}) i THEN
-    REPEAT1 (eresolve0_tac [@{thm asm_rl}, @{thm mp}] i)
+  fun iff_tac ctxt prems i =
+    resolve_tac ctxt (prems RL @{thms iffE}) i THEN
+    REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i)
 *}
 
+method_setup iff =
+  \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+
 lemma conj_cong:
   assumes "P <-> P'"
     and "P' ==> Q <-> Q'"
   shows "(P&Q) <-> (P'&Q')"
   apply (insert assms)
-  apply (assumption | rule iffI conjI | erule iffE conjE mp |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 (*Reversed congruence rule!   Used in ZF/Order*)
@@ -324,8 +326,7 @@
     and "P' ==> Q <-> Q'"
   shows "(Q&P) <-> (Q'&P')"
   apply (insert assms)
-  apply (assumption | rule iffI conjI | erule iffE conjE mp |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 lemma disj_cong:
@@ -340,8 +341,7 @@
     and "P' ==> Q <-> Q'"
   shows "(P-->Q) <-> (P'-->Q')"
   apply (insert assms)
-  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
   done
 
 lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
@@ -355,22 +355,19 @@
 lemma all_cong:
   assumes "!!x. P(x) <-> Q(x)"
   shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
-  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
   done
 
 lemma ex_cong:
   assumes "!!x. P(x) <-> Q(x)"
   shows "(EX x. P(x)) <-> (EX x. Q(x))"
-  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
   done
 
 lemma ex1_cong:
   assumes "!!x. P(x) <-> Q(x)"
   shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
-  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
   done
 
 (*** Equality rules ***)
diff -r 4862f3dc9540 -r c3ca292c1484 src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/FOL/intprover.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -6,7 +6,7 @@
 
 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
 
-Completeness (for propositional logic) is proved in 
+Completeness (for propositional logic) is proved in
 
 Roy Dyckhoff.
 Contraction-Free Sequent Calculi for Intuitionistic Logic.
@@ -15,7 +15,7 @@
 The approach was developed independently by Roy Dyckhoff and L C Paulson.
 *)
 
-signature INT_PROVER = 
+signature INT_PROVER =
 sig
   val best_tac: Proof.context -> int -> tactic
   val best_dup_tac: Proof.context -> int -> tactic
@@ -31,7 +31,7 @@
 end;
 
 
-structure IntPr : INT_PROVER   = 
+structure IntPr : INT_PROVER   =
 struct
 
 (*Negation is treated as a primitive symbol, with rules notI (introduction),
@@ -44,11 +44,11 @@
       (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
       (true, @{thm conjE}), (true, @{thm exE}),
       (false, @{thm conjI}), (true, @{thm conj_impE}),
-      (true, @{thm disj_impE}), (true, @{thm disjE}), 
+      (true, @{thm disj_impE}), (true, @{thm disjE}),
       (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
 
 val haz_brls =
-    [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), 
+    [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
       (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
       (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
 
@@ -65,7 +65,7 @@
 fun safe_step_tac ctxt =
   FIRST' [
     eq_assume_tac,
-    eq_mp_tac,
+    eq_mp_tac ctxt,
     bimatch_tac ctxt safe0_brls,
     hyp_subst_tac ctxt,
     bimatch_tac ctxt safep_brls];
@@ -75,7 +75,7 @@
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 fun inst_step_tac ctxt =
-  assume_tac ctxt APPEND' mp_tac APPEND' 
+  assume_tac ctxt APPEND' mp_tac ctxt APPEND'
   biresolve_tac ctxt (safe0_brls @ safep_brls);
 
 (*One safe or unsafe step. *)
diff -r 4862f3dc9540 -r c3ca292c1484 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/FOLP/IFOLP.thy	Fri Feb 13 23:39:25 2015 +0100
@@ -275,6 +275,7 @@
   fun mp_tac ctxt i =
     eresolve_tac ctxt [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac ctxt i
 *}
+method_setup mp = \<open>Scan.succeed (SIMPLE_METHOD' o mp_tac)\<close>
 
 (*Like mp_tac but instantiates no variables*)
 ML {*
@@ -360,23 +361,25 @@
 
 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
 ML {*
-fun iff_tac prems i =
-    resolve0_tac (prems RL [@{thm iffE}]) i THEN
-    REPEAT1 (eresolve0_tac [asm_rl, @{thm mp}] i)
+fun iff_tac ctxt prems i =
+    resolve_tac ctxt (prems RL [@{thm iffE}]) i THEN
+    REPEAT1 (eresolve_tac ctxt [asm_rl, @{thm mp}] i)
 *}
 
+method_setup iff =
+  \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+
 schematic_lemma conj_cong:
   assumes "p:P <-> P'"
     and "!!x. x:P' ==> q(x):Q <-> Q'"
   shows "?p:(P&Q) <-> (P'&Q')"
   apply (insert assms(1))
-  apply (assumption | rule iffI conjI |
-    erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 schematic_lemma disj_cong:
   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
-  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
+  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | mp)+
   done
 
 schematic_lemma imp_cong:
@@ -384,32 +387,29 @@
     and "!!x. x:P' ==> q(x):Q <-> Q'"
   shows "?p:(P-->Q) <-> (P'-->Q')"
   apply (insert assms(1))
-  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac @{context} 1 *} |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI impI | erule iffE | mp | iff assms)+
   done
 
 schematic_lemma iff_cong:
   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
-  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
+  apply (erule iffE | assumption | rule iffI | mp)+
   done
 
 schematic_lemma not_cong:
   "p:P <-> P' ==> ?p:~P <-> ~P'"
-  apply (assumption | rule iffI notI | tactic {* mp_tac @{context} 1 *} | erule iffE notE)+
+  apply (assumption | rule iffI notI | mp | erule iffE notE)+
   done
 
 schematic_lemma all_cong:
   assumes "!!x. f(x):P(x) <-> Q(x)"
   shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
-  apply (assumption | rule iffI allI | tactic {* mp_tac @{context} 1 *} | erule allE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI allI | mp | erule allE | iff assms)+
   done
 
 schematic_lemma ex_cong:
   assumes "!!x. f(x):P(x) <-> Q(x)"
   shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
-  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac @{context} 1 *} |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (erule exE | assumption | rule iffI exI | mp | iff assms)+
   done
 
 (*NOT PROVED
diff -r 4862f3dc9540 -r c3ca292c1484 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -35,24 +35,22 @@
        ('a * 'b) list -> ('a * 'b) list * ('a list * 'b list)
 
   val consts_in : term -> term list
-  val head_quantified_variable :
-     int -> thm -> (string * typ) option
+  val head_quantified_variable : Proof.context -> int -> thm -> (string * typ) option
   val push_allvar_in : string -> term -> term
   val strip_top_All_var : term -> (string * typ) * term
   val strip_top_All_vars : term -> (string * typ) list * term
   val strip_top_all_vars :
      (string * typ) list -> term -> (string * typ) list * term
-  val trace_tac' :
-     string ->
+  val trace_tac' : Proof.context -> string ->
      ('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
   val try_dest_Trueprop : term -> term
 
   val type_devar : ((indexname * sort) * typ) list -> term -> term
   val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
 
-  val batter : int -> tactic
-  val break_hypotheses : int -> tactic
-  val clause_breaker : int -> tactic
+  val batter_tac : Proof.context -> int -> tactic
+  val break_hypotheses_tac : Proof.context -> int -> tactic
+  val clause_breaker_tac : Proof.context -> int -> tactic
   (* val dist_all_and_tac : Proof.context -> int -> tactic *)(*FIXME unused*)
   val reassociate_conjs_tac : Proof.context -> int -> tactic
 
@@ -616,15 +614,15 @@
 
 (** Some tactics **)
 
-val break_hypotheses =
- ((REPEAT_DETERM o etac @{thm conjE})
-  THEN' (REPEAT_DETERM o etac @{thm disjE})
- ) #> CHANGED
+fun break_hypotheses_tac ctxt =
+  CHANGED o
+   ((REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) THEN'
+    (REPEAT_DETERM o eresolve_tac ctxt @{thms disjE}))
 
 (*Prove subgoals of form A ==> B1 | ... | A | ... | Bn*)
-val clause_breaker =
-  (REPEAT o (resolve0_tac [@{thm "disjI1"}, @{thm "disjI2"}, @{thm "conjI"}]))
-  THEN'  atac
+fun clause_breaker_tac ctxt =
+  (REPEAT o resolve_tac ctxt @{thms disjI1 disjI2 conjI}) THEN'
+  assume_tac ctxt
 
 (*
   Refines a subgoal have the form:
@@ -636,9 +634,9 @@
   where {A'1 .. A'm} is disjoint from {B1, ..., Aj, ..., Bi, ..., Ak, ...}
   (and solves the subgoal completely if the first set is empty)
 *)
-val batter =
-  break_hypotheses
-  THEN' K (ALLGOALS (TRY o clause_breaker))
+fun batter_tac ctxt i =
+  break_hypotheses_tac ctxt i THEN
+  ALLGOALS (TRY o clause_breaker_tac ctxt)
 
 (*Same idiom as ex_expander_tac*)
 fun dist_all_and_tac ctxt i =
@@ -669,11 +667,8 @@
         D
   This function returns "SOME X" if C = "! X. C'".
   If C has no quantification prefix, then returns NONE.*)
-fun head_quantified_variable i = fn st =>
+fun head_quantified_variable ctxt i = fn st =>
   let
-    val thy = Thm.theory_of_thm st
-    val ctxt = Proof_Context.init_global thy
-
     val gls =
       prop_of st
       |> Logic.strip_horn
@@ -779,10 +774,8 @@
 
 (** Tracing **)
 (*If "tac i st" succeeds then msg is printed to "trace" channel*)
-fun trace_tac' msg tac i st =
+fun trace_tac' ctxt msg tac i st =
   let
-    val thy = Thm.theory_of_thm st
-    val ctxt = Proof_Context.init_global thy
     val result = tac i st
   in
     if Config.get ctxt tptp_trace_reconstruction andalso
diff -r 4862f3dc9540 -r c3ca292c1484 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Feb 13 23:39:25 2015 +0100
@@ -223,7 +223,7 @@
         fun instantiates param =
            eres_inst_tac ctxt [(("x", 0), param)] thm
 
-        val quantified_var = head_quantified_variable i st
+        val quantified_var = head_quantified_variable ctxt i st
       in
         if is_none quantified_var then no_tac st
         else
@@ -1149,7 +1149,7 @@
     fun closure tac =
      (*batter fails if there's no toplevel disjunction in the
        hypothesis, so we also try atac*)
-      SOLVE o (tac THEN' (batter ORELSE' atac))
+      SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt))
     val search_tac =
       ASAP
         (rtac @{thm disjI1} APPEND' rtac @{thm disjI2})
@@ -1592,40 +1592,40 @@
 
         fun feat_to_tac feat =
           case feat of
-              Close_Branch => trace_tac' "mark: closer" efq_tac
-            | ConjI => trace_tac' "mark: conjI" (rtac @{thm conjI})
-            | King_Cong => trace_tac' "mark: expander_animal" (expander_animal ctxt)
-            | Break_Hypotheses => trace_tac' "mark: break_hypotheses" break_hypotheses
+              Close_Branch => trace_tac' ctxt "mark: closer" efq_tac
+            | ConjI => trace_tac' ctxt "mark: conjI" (rtac @{thm conjI})
+            | King_Cong => trace_tac' ctxt "mark: expander_animal" (expander_animal ctxt)
+            | Break_Hypotheses => trace_tac' ctxt "mark: break_hypotheses" (break_hypotheses_tac ctxt)
             | RemoveRedundantQuantifications => K all_tac
 (*
 FIXME Building this into the loop instead.. maybe not the ideal choice
             | RemoveRedundantQuantifications =>
-                trace_tac' "mark: strip_unused_variable_hyp"
+                trace_tac' ctxt "mark: strip_unused_variable_hyp"
                  (REPEAT_DETERM o remove_redundant_quantification_in_lit)
 *)
 
             | Assumption => atac
 (*FIXME both Existential_Free and Existential_Var run same code*)
-            | Existential_Free => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
-            | Existential_Var => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
-            | Universal => trace_tac' "mark: forall_pos" (forall_tac ctxt feats)
-            | Not_pos => trace_tac' "mark: not_pos" (dtac @{thm leo2_rules(9)})
-            | Not_neg => trace_tac' "mark: not_neg" (dtac @{thm leo2_rules(10)})
-            | Or_pos => trace_tac' "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
-            | Or_neg => trace_tac' "mark: or_neg" (dtac @{thm leo2_rules(7)})
-            | Equal_pos => trace_tac' "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
-            | Equal_neg => trace_tac' "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
-            | Donkey_Cong => trace_tac' "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
+            | Existential_Free => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
+            | Existential_Var => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
+            | Universal => trace_tac' ctxt "mark: forall_pos" (forall_tac ctxt feats)
+            | Not_pos => trace_tac' ctxt "mark: not_pos" (dtac @{thm leo2_rules(9)})
+            | Not_neg => trace_tac' ctxt "mark: not_neg" (dtac @{thm leo2_rules(10)})
+            | Or_pos => trace_tac' ctxt "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
+            | Or_neg => trace_tac' ctxt "mark: or_neg" (dtac @{thm leo2_rules(7)})
+            | Equal_pos => trace_tac' ctxt "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
+            | Equal_neg => trace_tac' ctxt "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
+            | Donkey_Cong => trace_tac' ctxt "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
 
-            | Extuni_Bool2 => trace_tac' "mark: extuni_bool2" (dtac @{thm extuni_bool2})
-            | Extuni_Bool1 => trace_tac' "mark: extuni_bool1" (dtac @{thm extuni_bool1})
-            | Extuni_Bind => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
-            | Extuni_Triv => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
-            | Extuni_Dec => trace_tac' "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
-            | Extuni_FlexRigid => trace_tac' "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
-            | Extuni_Func => trace_tac' "mark: extuni_func" (dtac @{thm extuni_func})
-            | Polarity_switch => trace_tac' "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
-            | Forall_special_pos => trace_tac' "mark: dorall_special_pos" extcnf_forall_special_pos_tac
+            | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dtac @{thm extuni_bool2})
+            | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dtac @{thm extuni_bool1})
+            | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
+            | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv})
+            | Extuni_Dec => trace_tac' ctxt "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
+            | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
+            | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dtac @{thm extuni_func})
+            | Polarity_switch => trace_tac' ctxt "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
+            | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" extcnf_forall_special_pos_tac
 
         val core_tac =
           get_loop_feats feats
@@ -1874,7 +1874,7 @@
 
       THEN (if have_loop_feats then
               REPEAT (CHANGED
-              ((ALLGOALS (TRY o clause_breaker)) (*brush away literals which don't change*)
+              ((ALLGOALS (TRY o clause_breaker_tac ctxt)) (*brush away literals which don't change*)
                THEN
                 (*FIXME move this to a different level?*)
                 (if loop_can_feature [Polarity_switch] feats then
diff -r 4862f3dc9540 -r c3ca292c1484 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -141,11 +141,6 @@
     (intros'', (local_defs, thy'))
   end
 
-(* TODO: same function occurs in inductive package *)
-fun select_disj 1 1 = []
-  | select_disj _ 1 = [rtac @{thm disjI1}]
-  | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1))
-
 fun introrulify thy ths = 
   let
     val ctxt = Proof_Context.init_global thy
@@ -168,7 +163,7 @@
         fun prove_introrule (index, (ps, introrule)) =
           let
             val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
-              THEN EVERY1 (select_disj (length disjuncts) (index + 1)) 
+              THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
               THEN (EVERY (map (fn y =>
                 rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
               THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
diff -r 4862f3dc9540 -r c3ca292c1484 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/Transfer/transfer.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -611,13 +611,15 @@
       |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
-fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve0_tac eq_rules)
+fun eq_rules_tac ctxt eq_rules =
+  TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules)
   THEN_ALL_NEW rtac @{thm is_equality_eq}
 
-fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt)
 
-fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt))
-  THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
+fun transfer_step_tac ctxt =
+  REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt)
+  THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt)))
 
 fun transfer_tac equiv ctxt i =
   let
@@ -635,7 +637,7 @@
         THEN_ALL_NEW
           (SOLVED'
             (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
-              (DETERM o eq_rules_tac eq_rules))
+              (DETERM o eq_rules_tac ctxt eq_rules))
             ORELSE' end_tac)) (i + 1)
         handle TERM (_, ts) => raise TERM (err_msg, ts)
   in
@@ -661,7 +663,7 @@
        ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
         THEN_ALL_NEW
          (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
-           (DETERM o eq_rules_tac eq_rules))) (i + 1),
+           (DETERM o eq_rules_tac ctxt eq_rules))) (i + 1),
        rtac @{thm refl} i]
   end)
 
@@ -689,7 +691,7 @@
       (rtac rule
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
-            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+            THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
@@ -725,7 +727,7 @@
       (rtac rule
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
-            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+            THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
diff -r 4862f3dc9540 -r c3ca292c1484 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/inductive.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -69,6 +69,7 @@
 signature INDUCTIVE =
 sig
   include BASIC_INDUCTIVE
+  val select_disj_tac: Proof.context -> int -> int -> int -> tactic
   type add_ind_def =
     inductive_flags ->
     term list -> (Attrib.binding * term) list -> thm list ->
@@ -168,9 +169,12 @@
   | mk_names a 1 = [a]
   | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
 
-fun select_disj 1 1 = []
-  | select_disj _ 1 = [resolve0_tac [disjI1]]
-  | select_disj n i = resolve0_tac [disjI2] :: select_disj (n - 1) (i - 1);
+fun select_disj_tac ctxt =
+  let
+    fun tacs 1 1 = []
+      | tacs _ 1 = [resolve_tac ctxt @{thms disjI1}]
+      | tacs n i = resolve_tac ctxt @{thms disjI2} :: tacs (n - 1) (i - 1);
+  in fn n => fn i => EVERY' (tacs n i) end;
 
 
 
@@ -403,7 +407,7 @@
       Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
        [rewrite_goals_tac ctxt rec_preds_defs,
         resolve_tac ctxt [unfold RS iffD2] 1,
-        EVERY1 (select_disj (length intr_ts) (i + 1)),
+        select_disj_tac ctxt (length intr_ts) (i + 1) 1,
         (*Not ares_tac, since refl must be tried before any equality assumptions;
           backtracking may occur if the premises have extra variables!*)
         DEPTH_SOLVE_1 (resolve_tac ctxt rules 1 APPEND assume_tac ctxt 1)])
@@ -495,7 +499,7 @@
           else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
         fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
-            EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
+            select_disj_tac ctxt'' (length c_intrs) (i + 1) 1 THEN
             EVERY (replicate (length params) (resolve_tac ctxt'' @{thms exI} 1)) THEN
             (if null prems then resolve_tac ctxt'' @{thms TrueI} 1
              else
diff -r 4862f3dc9540 -r c3ca292c1484 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -18,7 +18,7 @@
 sig
   val prep_simproc: theory -> string * string list * (Proof.context -> term -> thm option)
     -> simproc
-  val trans_tac: thm option -> tactic
+  val trans_tac: Proof.context -> thm option -> tactic
   val assoc_fold: Proof.context -> cterm -> thm option
   val combine_numerals: Proof.context -> cterm -> thm option
   val eq_cancel_numerals: Proof.context -> cterm -> thm option
@@ -48,8 +48,8 @@
 fun prep_simproc thy (name, pats, proc) =
   Simplifier.simproc_global thy name pats proc;
 
-fun trans_tac NONE  = all_tac
-  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
+fun trans_tac _ NONE  = all_tac
+  | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]);
 
 val mk_number = Arith_Data.mk_number;
 val mk_sum = Arith_Data.mk_sum;
diff -r 4862f3dc9540 -r c3ca292c1484 src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -29,7 +29,7 @@
                              as with < and <= but not = and div*)
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
-  val trans_tac: thm option -> tactic                (*applies the initial lemma*)
+  val trans_tac: Proof.context -> thm option -> tactic  (*applies the initial lemma*)
   val norm_tac: Proof.context -> tactic              (*proves the initial lemma*)
   val numeral_simp_tac: Proof.context -> tactic      (*proves the final theorem*)
   val simplify_meta_eq: Proof.context -> thm -> thm  (*simplifies the final theorem*)
@@ -72,7 +72,7 @@
   in
     Option.map (export o Data.simplify_meta_eq ctxt)
       (Data.prove_conv
-         [Data.trans_tac reshape, rtac Data.cancel 1,
+         [Data.trans_tac ctxt reshape, rtac Data.cancel 1,
           Data.numeral_simp_tac ctxt] ctxt prems (t', rhs))
   end
   (* FIXME avoid handling of generic exceptions *)
diff -r 4862f3dc9540 -r c3ca292c1484 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/Provers/Arith/cancel_numerals.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -36,7 +36,7 @@
   val bal_add2: thm
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
-  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
+  val trans_tac: Proof.context -> thm option -> tactic            (*applies the initial lemma*)
   val norm_tac: Proof.context -> tactic          (*proves the initial lemma*)
   val numeral_simp_tac: Proof.context -> tactic  (*proves the final theorem*)
   val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -92,12 +92,12 @@
     Option.map (export o Data.simplify_meta_eq ctxt)
       (if n2 <= n1 then
          Data.prove_conv
-           [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add1] 1,
+           [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1,
             Data.numeral_simp_tac ctxt] ctxt prems
            (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
        else
          Data.prove_conv
-           [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add2] 1,
+           [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1,
             Data.numeral_simp_tac ctxt] ctxt prems
            (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
   end
diff -r 4862f3dc9540 -r c3ca292c1484 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/Provers/Arith/combine_numerals.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -29,7 +29,7 @@
   val left_distrib: thm
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> term * term -> thm option
-  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
+  val trans_tac: Proof.context -> thm option -> tactic            (*applies the initial lemma*)
   val norm_tac: Proof.context -> tactic          (*proves the initial lemma*)
   val numeral_simp_tac: Proof.context -> tactic  (*proves the final theorem*)
   val simplify_meta_eq: Proof.context -> thm -> thm  (*simplifies the final theorem*)
@@ -83,7 +83,7 @@
   in
     Option.map (export o Data.simplify_meta_eq ctxt)
       (Data.prove_conv
-         [Data.trans_tac reshape, resolve_tac ctxt [Data.left_distrib] 1,
+         [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.left_distrib] 1,
           Data.numeral_simp_tac ctxt] ctxt
          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   end
diff -r 4862f3dc9540 -r c3ca292c1484 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/ZF/arith_data.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -9,7 +9,7 @@
   (*the main outcome*)
   val nat_cancel: simproc list
   (*tools for use in similar applications*)
-  val gen_trans_tac: thm -> thm option -> tactic
+  val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
   val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
   val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
   (*debugging*)
@@ -50,8 +50,8 @@
   | dest_sum tm = [tm];
 
 (*Apply the given rewrite (if present) just once*)
-fun gen_trans_tac th2 NONE      = all_tac
-  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve0_tac [th RS th2]);
+fun gen_trans_tac _ _ NONE = all_tac
+  | gen_trans_tac ctxt th2 (SOME th) = ALLGOALS (resolve_tac ctxt [th RS th2]);
 
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =
@@ -169,7 +169,7 @@
   val dest_bal = FOLogic.dest_eq
   val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
   val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
-  val trans_tac = gen_trans_tac @{thm iff_trans}
+  fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
   end;
 
 structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -182,7 +182,7 @@
   val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
   val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
   val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
-  val trans_tac = gen_trans_tac @{thm iff_trans}
+  fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
   end;
 
 structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -195,7 +195,7 @@
   val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
   val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
   val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
-  val trans_tac = gen_trans_tac @{thm trans}
+  fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
   end;
 
 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
diff -r 4862f3dc9540 -r c3ca292c1484 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Feb 12 12:46:50 2015 +0000
+++ b/src/ZF/int_arith.ML	Fri Feb 13 23:39:25 2015 +0100
@@ -151,12 +151,12 @@
 
 structure CancelNumeralsCommon =
   struct
-  val mk_sum            = (fn _ : typ => mk_sum)
-  val dest_sum          = dest_sum
-  val mk_coeff          = mk_coeff
-  val dest_coeff        = dest_coeff 1
-  val find_first_coeff  = find_first_coeff []
-  val trans_tac         = ArithData.gen_trans_tac @{thm iff_trans}
+  val mk_sum = (fn _ : typ => mk_sum)
+  val dest_sum = dest_sum
+  val mk_coeff = mk_coeff
+  val dest_coeff = dest_coeff 1
+  val find_first_coeff = find_first_coeff []
+  fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans}
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss @{context}
@@ -233,16 +233,16 @@
 
 structure CombineNumeralsData =
   struct
-  type coeff            = int
-  val iszero            = (fn x => x = 0)
-  val add               = op + 
-  val mk_sum            = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
-  val dest_sum          = dest_sum
-  val mk_coeff          = mk_coeff
-  val dest_coeff        = dest_coeff 1
-  val left_distrib      = @{thm left_zadd_zmult_distrib} RS @{thm trans}
-  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
-  val trans_tac         = ArithData.gen_trans_tac @{thm trans}
+  type coeff = int
+  val iszero = (fn x => x = 0)
+  val add = op + 
+  val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
+  val dest_sum = dest_sum
+  val mk_coeff = mk_coeff
+  val dest_coeff = dest_coeff 1
+  val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
+  val prove_conv = prove_conv_nohyps "int_combine_numerals"
+  fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss @{context}
@@ -281,34 +281,33 @@
 
 structure CombineNumeralsProdData =
 struct
-  type coeff            = int
-  val iszero            = (fn x => x = 0)
-  val add               = op *
-  val mk_sum            = (fn _ : typ => mk_prod)
-  val dest_sum          = dest_prod
-  fun mk_coeff(k,t) = if t=one then mk_numeral k
-                      else raise TERM("mk_coeff", [])
+  type coeff = int
+  val iszero = (fn x => x = 0)
+  val add = op *
+  val mk_sum = (fn _ : typ => mk_prod)
+  val dest_sum = dest_prod
+  fun mk_coeff(k,t) =
+    if t = one then mk_numeral k
+    else raise TERM("mk_coeff", [])
   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
-  val left_distrib      = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
-  val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
-  val trans_tac         = ArithData.gen_trans_tac @{thm trans}
-
-
+  val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
+  val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
+  fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
 
-val norm_ss1 =
-  simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps)
-val norm_ss2 =
-  simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
-  bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
-fun norm_tac ctxt =
-  ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
-  THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
+  val norm_ss1 =
+    simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps)
+  val norm_ss2 =
+    simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
+    bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
+  fun norm_tac ctxt =
+    ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
+    THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
 
-val numeral_simp_ss =
-  simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys)
-fun numeral_simp_tac ctxt =
-  ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
-val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
+  val numeral_simp_ss =
+    simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys)
+  fun numeral_simp_tac ctxt =
+    ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
 end;