name space groups are identified by serial, not serial_string;
authorwenzelm
Sun Oct 25 19:21:34 2009 +0100 (2009-10-25)
changeset 33171292970b42770
parent 33170 dd6d8d1f70d2
child 33172 61ee96bc9895
name space groups are identified by serial, not serial_string;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Oct 25 19:19:41 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Oct 25 19:21:34 2009 +0100
     1.3 @@ -567,7 +567,7 @@
     1.4      val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
     1.5  
     1.6      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     1.7 -        Inductive.add_inductive_global (serial_string ())
     1.8 +        Inductive.add_inductive_global (serial ())
     1.9            {quiet_mode = false, verbose = false, kind = Thm.internalK,
    1.10             alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
    1.11             skip_mono = true, fork_mono = false}
    1.12 @@ -1506,7 +1506,7 @@
    1.13  
    1.14      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
    1.15        thy10 |>
    1.16 -        Inductive.add_inductive_global (serial_string ())
    1.17 +        Inductive.add_inductive_global (serial ())
    1.18            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.19             alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
    1.20             skip_mono = true, fork_mono = false}
     2.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Oct 25 19:19:41 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Oct 25 19:21:34 2009 +0100
     2.3 @@ -280,7 +280,7 @@
     2.4        else primrec_err ("functions " ^ commas_quote names2 ^
     2.5          "\nare not mutually recursive");
     2.6      val (defs_thms, lthy') = lthy |>
     2.7 -      set_group ? LocalTheory.set_group (serial_string ()) |>
     2.8 +      set_group ? LocalTheory.set_group (serial ()) |>
     2.9        fold_map (apfst (snd o snd) oo
    2.10          LocalTheory.define Thm.definitionK o fst) defs';
    2.11      val qualify = Binding.qualify false
     3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 19:19:41 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 19:21:34 2009 +0100
     3.3 @@ -153,7 +153,7 @@
     3.4          (descr' ~~ recTs ~~ rec_sets') ([], 0);
     3.5  
     3.6      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     3.7 -        Inductive.add_inductive_global (serial_string ())
     3.8 +        Inductive.add_inductive_global (serial ())
     3.9            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    3.10              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    3.11              skip_mono = true, fork_mono = false}
     4.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sun Oct 25 19:19:41 2009 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sun Oct 25 19:21:34 2009 +0100
     4.3 @@ -170,7 +170,7 @@
     4.4          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
     4.5  
     4.6      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     4.7 -        Inductive.add_inductive_global (serial_string ())
     4.8 +        Inductive.add_inductive_global (serial ())
     4.9            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    4.10             alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
    4.11             skip_mono = true, fork_mono = false}
     5.1 --- a/src/HOL/Tools/Function/fun.ML	Sun Oct 25 19:19:41 2009 +0100
     5.2 +++ b/src/HOL/Tools/Function/fun.ML	Sun Oct 25 19:21:34 2009 +0100
     5.3 @@ -151,7 +151,7 @@
     5.4    domintros=false, partials=false, tailrec=false }
     5.5  
     5.6  fun gen_fun add config fixes statements int lthy =
     5.7 -  let val group = serial_string () in
     5.8 +  let val group = serial () in
     5.9      lthy
    5.10        |> LocalTheory.set_group group
    5.11        |> add fixes statements config
     6.1 --- a/src/HOL/Tools/Function/function.ML	Sun Oct 25 19:19:41 2009 +0100
     6.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Oct 25 19:21:34 2009 +0100
     6.3 @@ -118,7 +118,7 @@
     6.4          end
     6.5      in
     6.6        lthy
     6.7 -        |> is_external ? LocalTheory.set_group (serial_string ())
     6.8 +        |> is_external ? LocalTheory.set_group (serial ())
     6.9          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    6.10          |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    6.11      end
    6.12 @@ -173,12 +173,12 @@
    6.13  
    6.14  fun termination term_opt lthy =
    6.15    lthy
    6.16 -  |> LocalTheory.set_group (serial_string ())
    6.17 +  |> LocalTheory.set_group (serial ())
    6.18    |> termination_proof term_opt;
    6.19  
    6.20  fun termination_cmd term_opt lthy =
    6.21    lthy
    6.22 -  |> LocalTheory.set_group (serial_string ())
    6.23 +  |> LocalTheory.set_group (serial ())
    6.24    |> termination_proof_cmd term_opt;
    6.25  
    6.26  
     7.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sun Oct 25 19:19:41 2009 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sun Oct 25 19:21:34 2009 +0100
     7.3 @@ -367,7 +367,7 @@
     7.4          if is_some (try (map (cterm_of thy)) intr_ts) then
     7.5            let
     7.6              val (ind_result, thy') =
     7.7 -              Inductive.add_inductive_global (serial_string ())
     7.8 +              Inductive.add_inductive_global (serial ())
     7.9                  {quiet_mode = false, verbose = false, kind = Thm.internalK,
    7.10                    alt_name = Binding.empty, coind = false, no_elim = false,
    7.11                    no_ind = false, skip_mono = false, fork_mono = false}
     8.1 --- a/src/HOL/Tools/inductive.ML	Sun Oct 25 19:19:41 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive.ML	Sun Oct 25 19:21:34 2009 +0100
     8.3 @@ -47,7 +47,7 @@
     8.4      (Attrib.binding * string) list ->
     8.5      (Facts.ref * Attrib.src list) list ->
     8.6      bool -> local_theory -> inductive_result * local_theory
     8.7 -  val add_inductive_global: string -> inductive_flags ->
     8.8 +  val add_inductive_global: serial -> inductive_flags ->
     8.9      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    8.10      thm list -> theory -> inductive_result * theory
    8.11    val arities_of: thm -> (string * int) list
    8.12 @@ -859,7 +859,7 @@
    8.13        skip_mono = false, fork_mono = not int};
    8.14    in
    8.15      lthy
    8.16 -    |> LocalTheory.set_group (serial_string ())
    8.17 +    |> LocalTheory.set_group (serial ())
    8.18      |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
    8.19    end;
    8.20  
     9.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Oct 25 19:19:41 2009 +0100
     9.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Oct 25 19:21:34 2009 +0100
     9.3 @@ -351,7 +351,7 @@
     9.4      (** realizability predicate **)
     9.5  
     9.6      val (ind_info, thy3') = thy2 |>
     9.7 -      Inductive.add_inductive_global (serial_string ())
     9.8 +      Inductive.add_inductive_global (serial ())
     9.9          {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
    9.10            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    9.11          rlzpreds rlzparams (map (fn (rintr, intr) =>
    10.1 --- a/src/HOL/Tools/primrec.ML	Sun Oct 25 19:19:41 2009 +0100
    10.2 +++ b/src/HOL/Tools/primrec.ML	Sun Oct 25 19:21:34 2009 +0100
    10.3 @@ -275,7 +275,7 @@
    10.4          [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
    10.5    in
    10.6      lthy
    10.7 -    |> set_group ? LocalTheory.set_group (serial_string ())
    10.8 +    |> set_group ? LocalTheory.set_group (serial ())
    10.9      |> add_primrec_simple fixes (map snd spec)
   10.10      |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
   10.11            (attr_bindings prefix ~~ simps)