# HG changeset patch
# User wenzelm
# Date 1269282372 -3600
# Node ID 487b267433b1d2cb1a84aa1018c90f1af3c5323e
# Parent  387de5db0a74a8e5b17a9b15061ba016ee0ce061
inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;

diff -r 387de5db0a74 -r 487b267433b1 src/Pure/axclass.ML
--- 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;