# HG changeset patch
# User wenzelm
# Date 1379352440 -7200
# Node ID 5ccee1cb245a8c6a014d3e20d19b3d74054467d1
# Parent  6ede465b5be8e39f5787384d5ae94928ee3f9239
tuned signature;

diff -r 6ede465b5be8 -r 5ccee1cb245a src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 16 17:42:05 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 16 19:27:20 2013 +0200
@@ -8,10 +8,11 @@
 signature FUN_CASES =
 sig
   val mk_fun_cases : Proof.context -> term -> thm
+  val fun_cases_cmd: ((binding * Args.src list) * string list) list -> local_theory ->
+    (string * thm list) list * local_theory
   (* FIXME regular ML interface for fun_cases *)
 end;
 
-
 structure Fun_Cases : FUN_CASES =
 struct
 
@@ -71,6 +72,8 @@
          (subst_Vars subst t) ctxt)
   end;
 
+in
+
 fun fun_cases_cmd args lthy =
   let
     val thy = Proof_Context.theory_of lthy
@@ -83,11 +86,9 @@
     val facts = map2 (fn ((a,atts), _) => fn thms =>
       ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
   in
-    lthy |> Local_Theory.notes facts |>> map snd
+    lthy |> Local_Theory.notes facts
   end;
 
-in
-
 val _ =
   Outer_Syntax.local_theory @{command_spec "fun_cases"}
     "automatic derivation of simplified elimination rules for function equations"