# HG changeset patch
# User wenzelm
# Date 1423651359 -3600
# Node ID 82ab8168d940487d0e0d39a4cf83d511896d3a3b
# Parent  7c433cca8fe0895eb2b4a80cc0026b8e406d57ee
proper context;
eliminated clone;

diff -r 7c433cca8fe0 -r 82ab8168d940 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Feb 11 11:26:17 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Feb 11 11:42:39 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 7c433cca8fe0 -r 82ab8168d940 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Feb 11 11:26:17 2015 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Feb 11 11:42:39 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