--- 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}
--- 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
--- 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}
--- 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}
--- 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
--- 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;
--- 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}
--- 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;
--- 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) =>
--- 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)