# HG changeset patch
# User wenzelm
# Date 1256494894 -3600
# Node ID 292970b42770b6767cd918faab295be3d9c304be
# Parent  dd6d8d1f70d2bec5397656fd23cebf2491038ec2
name space groups are identified by serial, not serial_string;

diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -567,7 +567,7 @@
     val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
-        Inductive.add_inductive_global (serial_string ())
+        Inductive.add_inductive_global (serial ())
           {quiet_mode = false, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
@@ -1506,7 +1506,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10 |>
-        Inductive.add_inductive_global (serial_string ())
+        Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
            skip_mono = true, fork_mono = false}
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -280,7 +280,7 @@
       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
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -153,7 +153,7 @@
         (descr' ~~ recTs ~~ rec_sets') ([], 0);
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
-        Inductive.add_inductive_global (serial_string ())
+        Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
             skip_mono = true, fork_mono = false}
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -170,7 +170,7 @@
         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
-        Inductive.add_inductive_global (serial_string ())
+        Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -151,7 +151,7 @@
   domintros=false, partials=false, tailrec=false }
 
 fun gen_fun add config fixes statements int lthy =
-  let val group = serial_string () in
+  let val group = serial () in
     lthy
       |> LocalTheory.set_group group
       |> add fixes statements config
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -118,7 +118,7 @@
         end
     in
       lthy
-        |> is_external ? LocalTheory.set_group (serial_string ())
+        |> is_external ? LocalTheory.set_group (serial ())
         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
     end
@@ -173,12 +173,12 @@
 
 fun termination term_opt lthy =
   lthy
-  |> LocalTheory.set_group (serial_string ())
+  |> LocalTheory.set_group (serial ())
   |> termination_proof term_opt;
 
 fun termination_cmd term_opt lthy =
   lthy
-  |> LocalTheory.set_group (serial_string ())
+  |> LocalTheory.set_group (serial ())
   |> termination_proof_cmd term_opt;
 
 
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -367,7 +367,7 @@
         if is_some (try (map (cterm_of thy)) intr_ts) then
           let
             val (ind_result, thy') =
-              Inductive.add_inductive_global (serial_string ())
+              Inductive.add_inductive_global (serial ())
                 {quiet_mode = false, verbose = false, kind = Thm.internalK,
                   alt_name = Binding.empty, coind = false, no_elim = false,
                   no_ind = false, skip_mono = false, fork_mono = false}
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -47,7 +47,7 @@
     (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
-  val add_inductive_global: string -> inductive_flags ->
+  val add_inductive_global: serial -> inductive_flags ->
     ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> theory -> inductive_result * theory
   val arities_of: thm -> (string * int) list
@@ -859,7 +859,7 @@
       skip_mono = false, fork_mono = not int};
   in
     lthy
-    |> LocalTheory.set_group (serial_string ())
+    |> LocalTheory.set_group (serial ())
     |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
   end;
 
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -351,7 +351,7 @@
     (** realizability predicate **)
 
     val (ind_info, thy3') = thy2 |>
-      Inductive.add_inductive_global (serial_string ())
+      Inductive.add_inductive_global (serial ())
         {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
           coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
diff -r dd6d8d1f70d2 -r 292970b42770 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Sun Oct 25 19:19:41 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Sun Oct 25 19:21:34 2009 +0100
@@ -275,7 +275,7 @@
         [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
   in
     lthy
-    |> set_group ? LocalTheory.set_group (serial_string ())
+    |> set_group ? LocalTheory.set_group (serial ())
     |> add_primrec_simple fixes (map snd spec)
     |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
           (attr_bindings prefix ~~ simps)