# HG changeset patch
# User wenzelm
# Date 1380540905 -7200
# Node ID 28fefe1d67492bc7cfde9685a662f1b78da0fac0
# Parent  8b70dba5572ff47ac96336a91afc041b9ce6e316
tuned signature;

diff -r 8b70dba5572f -r 28fefe1d6749 src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:29:09 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:35:05 2013 +0200
@@ -1,16 +1,16 @@
 (*  Title:      HOL/Tools/Function/fun_cases.ML
     Author:     Manuel Eberl, TU Muenchen
 
-Provide the fun_cases command for generating specialised elimination
-rules for function package functions.
+The fun_cases command for generating specialised elimination rules for
+function package functions.
 *)
 
 signature FUN_CASES =
 sig
-  val mk_fun_cases : Proof.context -> term -> thm
-  val fun_cases: (Attrib.binding * string list) list -> local_theory ->
+  val mk_fun_cases: Proof.context -> term -> thm
+  val fun_cases: (Attrib.binding * term list) list -> local_theory ->
     thm list list * local_theory
-  val fun_cases_i: (Attrib.binding * term list) list -> local_theory ->
+  val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
     thm list list * local_theory
 end;
 
@@ -68,13 +68,13 @@
         args thmss;
   in lthy |> Local_Theory.notes facts |>> map snd end;
 
-val fun_cases = gen_fun_cases Attrib.intern_src Syntax.read_prop;
-val fun_cases_i = gen_fun_cases (K I) Syntax.check_prop;
+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"
-    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases));
+    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
 
 end;