tuned signature;

--- a/src/Pure/Isar/rule_cases.ML	Thu Jun 25 15:56:33 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Thu Jun 25 16:14:00 2015 +0200
@@ -27,10 +27,9 @@
     cases: (string * T) list}
   val case_hypsN: string
   val strip_params: term -> (string * typ) list
-  val make_common: Proof.context -> term ->
-    ((string * string list) * string list) list -> cases
-  val make_nested: Proof.context -> term -> term ->
-    ((string * string list) * string list) list -> cases
+  type info = ((string * string list) * string list) list
+  val make_common: Proof.context -> term -> info -> cases
+  val make_nested: Proof.context -> term -> term -> info -> cases
   val apply: term list -> T -> T
   val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
@@ -51,7 +50,7 @@
   val cases_open: attribute
   val internalize_params: thm -> thm
   val save: thm -> thm -> thm
-  val get: thm -> ((string * string list) * string list) list * int
+  val get: thm -> info * int
   val rename_params: string list list -> thm -> thm
   val params: string list list -> attribute
   val mutual_rule: Proof.context -> thm list -> (int list * thm) option
@@ -77,6 +76,8 @@
 
 val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
 
+type info = ((string * string list) * string list) list;
+
 local
 
 fun app us t = Term.betapplys (t, us);
@@ -221,13 +222,13 @@
 
 in
 
-fun consume ctxt defs facts ((xx, n), th) =
+fun consume ctxt defs facts ((a, n), th) =
   let val m = Int.min (length facts, n) in
     th
     |> unfold_prems ctxt n defs
     |> unfold_prems_concls ctxt defs
     |> Drule.multi_resolve (SOME ctxt) (take m facts)
-    |> Seq.map (pair (xx, (n - m, drop m facts)))
+    |> Seq.map (pair (a, (n - m, drop m facts)))
   end;
 
 end;

--- a/src/Tools/induct.ML	Thu Jun 25 15:56:33 2015 +0200
+++ b/src/Tools/induct.ML	Thu Jun 25 16:14:00 2015 +0200
@@ -74,8 +74,7 @@
   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
-  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
-  val gen_induct_tac: (case_data * thm -> case_data * thm) ->
+  val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
     Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
@@ -735,8 +734,6 @@
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
-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) =>
     let