--- 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 =
--- 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 = {*
--- 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 =
--- 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