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 =