src/HOL/Nominal/nominal_primrec.ML

   | common_prefix eq (x :: xs, y :: ys) =
       if eq (x, y) then x :: common_prefix eq (xs, ys) else [];
 
 local
 
-fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
+fun gen_primrec prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
   let
     val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
     val fixes = List.take (fixes', length raw_fixes);
     val (names_atts, spec') = split_list spec;
     val eqns' = map unquantify spec'

     val names2 = map fst eqns;
     val _ = if eq_set (op =) (names1, names2) then ()
       else primrec_err ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val (defs_thms, lthy') = lthy |>
-      set_group ? Local_Theory.set_group (serial ()) |>
       fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
     val qualify = Binding.qualify false
       (space_implode "_" (map (Long_Name.base_name o #1) defs));
     val names_atts' = map (apfst qualify) names_atts;
     val cert = cterm_of (ProofContext.theory_of lthy');

     Seq.hd
   end;
 
 in
 
-val add_primrec = gen_primrec false Specification.check_spec (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
+val add_primrec = gen_primrec Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
 
 end;
 
 
 (* outer syntax *)