# HG changeset patch
# User wenzelm
# Date 1203953477 -3600
# Node ID 14f6dbb195c4169fda9b1ae6e1666f959db2fae8
# Parent  fe2d24c26e0c9dc6b2613f535c668a9641979d67
LocalTheory.set_group for user command;

diff -r fe2d24c26e0c -r 14f6dbb195c4 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Feb 25 16:31:15 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Feb 25 16:31:17 2008 +0100
@@ -305,6 +305,7 @@
 
 fun fun_cmd config fixes statements flags lthy =
     lthy
+      |> LocalTheory.set_group (serial_string ())
       |> FundefPackage.add_fundef fixes statements config flags
       |> by_pat_completeness_simp
       |> LocalTheory.reinit
diff -r fe2d24c26e0c -r 14f6dbb195c4 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 25 16:31:15 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 25 16:31:17 2008 +0100
@@ -90,7 +90,7 @@
     end
 
 
-fun gen_add_fundef prep fixspec eqnss config flags lthy =
+fun gen_add_fundef set_group prep fixspec eqnss config flags lthy =
     let
       val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
@@ -103,6 +103,7 @@
       val afterqed = fundef_afterqed config fixes post defname cont sort_cont cnames
     in
       lthy
+        |> set_group ? LocalTheory.set_group (serial_string ())
         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
     end
@@ -150,8 +151,8 @@
     end
 
 
-val add_fundef = gen_add_fundef Specification.read_specification
-val add_fundef_i = gen_add_fundef Specification.check_specification
+val add_fundef = gen_add_fundef true Specification.read_specification
+val add_fundef_i = gen_add_fundef false Specification.check_specification
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)
diff -r fe2d24c26e0c -r 14f6dbb195c4 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Mon Feb 25 16:31:15 2008 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Mon Feb 25 16:31:17 2008 +0100
@@ -43,7 +43,6 @@
           InductivePackage.add_inductive_i
             {verbose = ! Toplevel.debug,
               kind = Thm.internalK,
-              group = serial_string (),   (* FIXME pass proper group (!?) *)
               alt_name = "",
               coind = false,
               no_elim = false,
diff -r fe2d24c26e0c -r 14f6dbb195c4 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Mon Feb 25 16:31:15 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Mon Feb 25 16:31:17 2008 +0100
@@ -221,7 +221,7 @@
     val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
   in map (fn (name_attr, t) => (name_attr, [Goal.prove ctxt [] [] t tac])) end;
 
-fun gen_primrec prep_spec raw_fixes raw_spec lthy =
+fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
   let
     val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
     val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
@@ -248,6 +248,7 @@
       [Simplifier.simp_add, RecfunCodegen.add NONE];
   in
     lthy
+    |> set_group ? LocalTheory.set_group (serial_string ())
     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
@@ -261,8 +262,8 @@
 
 in
 
-val add_primrec = gen_primrec Specification.check_specification;
-val add_primrec_cmd = gen_primrec Specification.read_specification;
+val add_primrec = gen_primrec false Specification.check_specification;
+val add_primrec_cmd = gen_primrec true Specification.read_specification;
 
 end;