# HG changeset patch
# User wenzelm
# Date 1428515932 -7200
# Node ID ea06500bb0925d112f686338211b77a75c25a7a9
# Parent  e9f73d87d904d6ba6d834f927470961287a9c914
tuned signature;

diff -r e9f73d87d904 -r ea06500bb092 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Wed Apr 08 19:39:08 2015 +0200
+++ b/src/HOL/Tools/coinduction.ML	Wed Apr 08 19:58:52 2015 +0200
@@ -37,7 +37,7 @@
     (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
   end;
 
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
+fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _) =>
   let
     val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
     fun find_coinduct t =
diff -r e9f73d87d904 -r ea06500bb092 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:39:08 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:58:52 2015 +0200
@@ -443,7 +443,7 @@
 qed
 
 ML {*
-  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
+  fun eventually_elim_tac ctxt thms st = SUBGOAL_CASES (fn _ =>
     let
       val mp_thms = thms RL [@{thm eventually_rev_mp}]
       val raw_elim_thm =
@@ -454,7 +454,7 @@
       val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
     in
       CASES cases (rtac raw_elim_thm 1)
-    end) 1
+    end) 1 st
 *}
 
 method_setup eventually_elim = {*
diff -r e9f73d87d904 -r ea06500bb092 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Apr 08 19:39:08 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Apr 08 19:58:52 2015 +0200
@@ -13,7 +13,7 @@
   type cases_tactic = thm -> cases_state Seq.seq
   val CASES: cases -> tactic -> cases_tactic
   val EMPTY_CASES: tactic -> cases_tactic
-  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
+  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
   val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
 end
 
@@ -192,7 +192,7 @@
 
 fun SUBGOAL_CASES tac i st =
   (case try Logic.nth_prem (i, Thm.prop_of st) of
-    SOME goal => tac (goal, i, st) st
+    SOME goal => tac (goal, i) st
   | NONE => Seq.empty);
 
 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
diff -r e9f73d87d904 -r ea06500bb092 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Apr 08 19:39:08 2015 +0200
+++ b/src/Tools/induct.ML	Wed Apr 08 19:58:52 2015 +0200
@@ -731,7 +731,7 @@
 type case_data = (((string * string list) * string list) list * int);
 
 fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
-  SUBGOAL_CASES (fn (_, i, st) =>
+  SUBGOAL_CASES (fn (_, i) =>
     let
       val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
       val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
@@ -820,7 +820,7 @@
 
 in
 
-fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
+fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
   let
     fun inst_rule r =
       if null inst then `Rule_Cases.get r