--- a/src/HOL/Tools/function_package/fundef_datatype.ML Thu Oct 12 22:03:33 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Thu Oct 12 22:57:15 2006 +0200
@@ -14,8 +14,6 @@
val setup : theory -> theory
end
-
-
structure FundefDatatype : FUNDEF_DATATYPE =
struct
@@ -167,6 +165,7 @@
Proof.global_terminal_proof
(Method.Basic (K pat_completeness),
SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
+ (* FIXME avoid dynamic scoping of method name! *)
val setup =
@@ -175,14 +174,9 @@
-
-
local structure P = OuterParse and K = OuterKeyword in
-fun local_theory_to_proof f =
- Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
-
fun or_list1 s = P.enum1 "|" s
val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
@@ -192,17 +186,12 @@
OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
>> (fn ((target, fixes), statements) =>
- Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements FundefCommon.fun_config
- #> by_pat_completeness_simp)));
+ Toplevel.print o
+ Toplevel.local_theory target
+ (FundefPackage.add_fundef fixes statements FundefCommon.fun_config
+ #> by_pat_completeness_simp)));
val _ = OuterSyntax.add_parsers [funP];
end
-
-
-
-
-
-
-
end