src/HOL/Nominal/nominal_primrec.ML

     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 ? LocalTheory.set_group (serial_string ()) |>
+      set_group ? LocalTheory.set_group (serial ()) |>
       fold_map (apfst (snd o snd) oo
         LocalTheory.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;