# HG changeset patch
# User wenzelm
# Date 1362069515 -3600
# Node ID dfe469293eb4f827cea694a28b781fb9d19eb2c4
# Parent  536a5603a1381f56a8f87fc6c3ccb38eed75306e
discontinued empty name bindings in 'axiomatization';

diff -r 536a5603a138 -r dfe469293eb4 NEWS
--- a/NEWS	Thu Feb 28 17:14:55 2013 +0100
+++ b/NEWS	Thu Feb 28 17:38:35 2013 +0100
@@ -20,6 +20,9 @@
 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
 instead, while observing its uniform scope for polymorphism.
 
+* Discontinued empty name bindings in 'axiomatization'.
+INCOMPATIBILITY.
+
 
 *** HOL ***
 
diff -r 536a5603a138 -r dfe469293eb4 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Feb 28 17:14:55 2013 +0100
+++ b/src/Pure/more_thm.ML	Thu Feb 28 17:38:35 2013 +0100
@@ -351,16 +351,14 @@
 
 fun add_axiom ctxt (b, prop) thy =
   let
-    val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
-
     val _ = Sign.no_vars ctxt prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
 
     val thy' = thy
-      |> Theory.add_axiom ctxt (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
-    val axm_name = Sign.full_name thy' b';
+      |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
+    val axm_name = Sign.full_name thy' b;
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'