--- a/src/Pure/Isar/rule_cases.ML Mon Mar 09 11:32:32 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML Mon Mar 09 20:33:33 2015 +0100
@@ -9,7 +9,8 @@
signature BASIC_RULE_CASES =
sig
type cases
- type cases_tactic
+ type cases_state = cases * thm
+ type cases_tactic = thm -> cases_state Seq.seq
val CASES: cases -> tactic -> cases_tactic
val NO_CASES: tactic -> cases_tactic
val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
@@ -183,7 +184,8 @@
(** tactics with cases **)
-type cases_tactic = thm -> (cases * thm) Seq.seq;
+type cases_state = cases * thm;
+type cases_tactic = thm -> cases_state Seq.seq;
fun CASES cases tac st = Seq.map (pair cases) (tac st);
fun NO_CASES tac = CASES [] tac;