src/HOL/Tools/primrec_package.ML

     val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
     fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
     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
       orelse exists (fn ((w, _), _) => v = w) fixes) o snd) spec [];
     val tnames = distinct (op =) (map (#1 o snd) eqns);

       (space_implode "_" (map (Sign.base_name o #1) defs));
     val simp_atts = map (Attrib.internal o K)
       [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)
     |-> (fn simps' => LocalTheory.note Thm.theoremK
           ((qualify "simps", simp_atts), maps snd simps'))

      of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
       | NONE => ""));
 
 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;
 
 
 (* outer syntax *)