inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;

--- a/src/Pure/axclass.ML	Mon Mar 22 19:25:14 2010 +0100
+++ b/src/Pure/axclass.ML	Mon Mar 22 19:26:12 2010 +0100
@@ -514,6 +514,12 @@
 
 local
 
+(* old-style axioms *)
+
+fun add_axiom (b, prop) =
+  Thm.add_axiom (b, prop) #->
+  (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
+
 fun axiomatize prep mk name add raw_args thy =
   let
     val args = prep thy raw_args;
@@ -521,7 +527,7 @@
     val names = name args;
   in
     thy
-    |> fold_map Drule.add_axiom (map Binding.name names ~~ specs)
+    |> fold_map add_axiom (map Binding.name names ~~ specs)
     |-> fold add
   end;