--- 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"