--- a/src/HOL/Tools/function_package/fundef_datatype.ML Wed Feb 27 21:41:08 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Wed Feb 27 21:46:13 2008 +0100
@@ -297,19 +297,22 @@
#> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
-val fun_config = FundefConfig { sequential=true, default="%x. arbitrary",
+val fun_config = FundefConfig { sequential=true, default="%x. arbitrary" (* FIXME dynamic scoping *),
target=NONE, domintros=false, tailrec=false }
local structure P = OuterParse and K = OuterKeyword in
fun fun_cmd config fixes statements flags lthy =
+ let val group = serial_string () in
lthy
- |> LocalTheory.set_group (serial_string ())
+ |> LocalTheory.set_group group
|> FundefPackage.add_fundef fixes statements config flags
|> by_pat_completeness_simp
|> LocalTheory.reinit
+ |> LocalTheory.set_group group
|> termination_by_lexicographic_order
+ end;
val _ =
OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Feb 27 21:41:08 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Feb 27 21:46:13 2008 +0100
@@ -150,6 +150,10 @@
|> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
end
+fun termination_cmd term_opt lthy =
+ lthy
+ |> LocalTheory.set_group (serial_string ())
+ |> setup_termination_proof term_opt;
val add_fundef = gen_add_fundef true Specification.read_specification
val add_fundef_i = gen_add_fundef false Specification.check_specification
@@ -272,7 +276,7 @@
(P.opt_target -- Scan.option P.term
>> (fn (target, name) =>
Toplevel.print o
- Toplevel.local_theory_to_proof target (setup_termination_proof name)));
+ Toplevel.local_theory_to_proof target (termination_cmd name)));
end;