tuned signature;

--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:45:17 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 14:17:27 2013 +0200
@@ -9,9 +9,9 @@
 sig
   val mk_fun_cases: Proof.context -> term -> thm
   val fun_cases: (Attrib.binding * term list) list -> local_theory ->
-    thm list list * local_theory
+    (string * thm list) list * local_theory
   val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
-    thm list list * local_theory
+    (string * thm list) list * local_theory
 end;
 
 structure Fun_Cases : FUN_CASES =
@@ -50,14 +50,14 @@
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
         args thmss;
-  in lthy |> Local_Theory.notes facts |>> map snd end;
+  in lthy |> Local_Theory.notes facts end;
 
 val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
 val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "fun_cases"}
-    "automatic derivation of simplified elimination rules for function equations"
+    "create simplified instances of elimination rules for function equations"
     (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
 
 end;

--- a/src/HOL/Tools/inductive.ML	Mon Sep 30 13:45:17 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Sep 30 14:17:27 2013 +0200
@@ -35,9 +35,13 @@
   val inductive_forall_def: thm
   val rulify: Proof.context -> thm -> thm
   val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
-    thm list list * local_theory
+    (string * thm list) list * local_theory
   val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
-    thm list list * local_theory
+    (string * thm list) list * local_theory
+  val inductive_simps: (Attrib.binding * string list) list -> local_theory ->
+    (string * thm list) list * local_theory
+  val inductive_simps_i: (Attrib.binding * term list) list -> local_theory ->
+    (string * thm list) list * local_theory
   type inductive_flags =
     {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
       no_elim: bool, no_ind: bool, skip_mono: bool}
@@ -578,7 +582,7 @@
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
         args thmss;
-  in lthy |> Local_Theory.notes facts |>> map snd end;
+  in lthy |> Local_Theory.notes facts end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
@@ -634,7 +638,7 @@
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
-  in lthy |> Local_Theory.notes facts |>> map snd end;
+  in lthy |> Local_Theory.notes facts end;
 
 val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
 val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;