# HG changeset patch
# User wenzelm
# Date 1269196219 -3600
# Node ID f2126d4d048662d18448c00b2a45b8e63ef5f506
# Parent  4e3fe0b8687bd2e7832bcadb821124f2016255cb
more explicit invented name;

diff -r 4e3fe0b8687b -r f2126d4d0486 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Mar 21 19:28:25 2010 +0100
+++ b/src/Pure/more_thm.ML	Sun Mar 21 19:30:19 2010 +0100
@@ -324,7 +324,7 @@
 
 fun add_axiom (b, prop) thy =
   let
-    val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b;
+    val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
     val thy' = thy |> Theory.add_axioms_i [(b', prop)];
     val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b'));
   in (axm, thy') end;