# HG changeset patch
# User wenzelm
# Date 1268345222 -3600
# Node ID 9dc39bad4f4dab5afb24e4843972db92dd57143e
# Parent  68f7603f2aeb46f7ebb9f0dce85ff7fb7c379b5a
tuned;

diff -r 68f7603f2aeb -r 9dc39bad4f4d src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Mar 11 18:52:50 2010 +0100
+++ b/src/Pure/more_thm.ML	Thu Mar 11 23:07:02 2010 +0100
@@ -324,8 +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 ("axiom_" ^ serial_string ()) else b;
     val thy' = thy |> Theory.add_axioms_i [(b', prop)];
     val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
   in (axm, thy') end;