# HG changeset patch
# User wenzelm
# Date 1146430211 -7200
# Node ID 73361110b570fcc9bb9c8f82d8205424f37e5268
# Parent  dcc4b1d5b73220d0333ad5fa5d6eebd798328647
tuned;

diff -r dcc4b1d5b732 -r 73361110b570 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Apr 30 22:50:10 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun Apr 30 22:50:11 2006 +0200
@@ -214,7 +214,7 @@
 
 fun add_axiom hyps (name, prop) thy =
   let
-    val name' = if name = "" then "axiom_" ^ string_of_int (serial ()) else name;
+    val name' = if name = "" then "axiom_" ^ serial_string () else name;
     val frees = rev ([] |> Term.add_frees prop |> fold Term.add_frees hyps);
     val prop' = Term.list_all_free (frees, Logic.list_implies (hyps, prop));
     val thy' = thy |> Theory.add_axioms_i [(name', prop')];