1.1 --- a/NEWS	Thu Feb 28 17:14:55 2013 +0100
     1.2 +++ b/NEWS	Thu Feb 28 17:38:35 2013 +0100
     1.3 @@ -20,6 +20,9 @@
     1.4  legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
     1.5  instead, while observing its uniform scope for polymorphism.
     1.6  
     1.7 +* Discontinued empty name bindings in 'axiomatization'.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  

     2.1 --- a/src/Pure/more_thm.ML	Thu Feb 28 17:14:55 2013 +0100
     2.2 +++ b/src/Pure/more_thm.ML	Thu Feb 28 17:38:35 2013 +0100
     2.3 @@ -351,16 +351,14 @@
     2.4  
     2.5  fun add_axiom ctxt (b, prop) thy =
     2.6    let
     2.7 -    val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
     2.8 -
     2.9      val _ = Sign.no_vars ctxt prop;
    2.10      val (strip, recover, prop') = stripped_sorts thy prop;
    2.11      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
    2.12      val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
    2.13  
    2.14      val thy' = thy
    2.15 -      |> Theory.add_axiom ctxt (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
    2.16 -    val axm_name = Sign.full_name thy' b';
    2.17 +      |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
    2.18 +    val axm_name = Sign.full_name thy' b;
    2.19      val axm' = Thm.axiom thy' axm_name;
    2.20      val thm =
    2.21        Thm.instantiate (recover, []) axm'