src/Pure/Isar/isar_cmd.ML

--- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 22 15:07:07 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 22 19:23:03 2010 +0100
@@ -166,7 +166,7 @@
 
 (* old-style axioms *)
 
-val add_axioms = fold (fn (b, ax) => snd o Specification.axiomatization_cmd [] [(b, [ax])]);
+val add_axioms = fold (snd oo Specification.axiom_cmd);
 
 fun add_defs ((unchecked, overloaded), args) thy =
   thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded