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