# HG changeset patch
# User wenzelm
# Date 1380543447 -7200
# Node ID 1d457fc83f5cb7f71dc47caf8c211160254de30a
# Parent  4237859c186d90743607b6a89fb125adef9de4c0
tuned signature;

diff -r 4237859c186d -r 1d457fc83f5c src/HOL/Tools/Function/fun_cases.ML
--- 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;
diff -r 4237859c186d -r 1d457fc83f5c src/HOL/Tools/inductive.ML
--- 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;