# HG changeset patch
# User wenzelm
# Date 1204145173 -3600
# Node ID 5426a823455cd6fc8e0849ec72146a918f7cb5e4
# Parent  66e6b967ccf10521351c8131ebfbb75db6edb613
more precise handling of "group" for termination;

diff -r 66e6b967ccf1 -r 5426a823455c src/HOL/Tools/function_package/fundef_datatype.ML
--- 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
diff -r 66e6b967ccf1 -r 5426a823455c src/HOL/Tools/function_package/fundef_package.ML
--- 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;