replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -241,7 +241,7 @@
   let val (used, new) = mark_axioms thy (name_axioms axs)
   in
     thy
-    |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) new)
+    |> fold_map (Drule.add_axiom o apfst Binding.name) new
     |-> Context.theory_map o fold Boogie_Axioms.add_thm
     |> log verbose "The following axioms were added:" (map fst new)
     |> (fn thy' => log verbose "The following axioms already existed:"

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -182,8 +182,8 @@
          val new_defs = map new_def assms
          val (definition, thy') = thy
           |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> PureThy.add_axioms (map_index
-              (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), t), [])) new_defs)
+          |> fold_map Drule.add_axiom (map_index
+              (fn (i, t) => (Binding.name (constname ^ "_def" ^ string_of_int i), t)) new_defs)
         in
           (lhs, ((full_constname, definition) :: defs, thy'))
         end

--- a/src/HOL/Tools/choice_specification.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -44,9 +44,9 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
+                    val (thm, thy') = Drule.add_axiom (Binding.name axname, HOLogic.mk_Trueprop tm) thy
                 in
-                    (thy',hd thms)
+                    (thy', thm)
                 end
               | process ((thname,cname,covld)::cos) (thy,tm) =
                 case tm of

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -54,13 +54,8 @@
     val abs_iso_bind = Binding.qualified true "abs_iso" dbind;
     val rep_iso_bind = Binding.qualified true "rep_iso" dbind;
 
-    val (abs_iso_thm, thy) =
-        yield_singleton PureThy.add_axioms
-        ((abs_iso_bind, abs_iso_eqn), []) thy;
-
-    val (rep_iso_thm, thy) =
-        yield_singleton PureThy.add_axioms
-        ((rep_iso_bind, rep_iso_eqn), []) thy;
+    val (abs_iso_thm, thy) = Drule.add_axiom (abs_iso_bind, abs_iso_eqn) thy;
+    val (rep_iso_thm, thy) = Drule.add_axiom (rep_iso_bind, rep_iso_eqn) thy;
 
     val result =
         {
@@ -88,9 +83,7 @@
 
     val lub_take_bind = Binding.qualified true "lub_take" dbind;
 
-    val (lub_take_thm, thy) =
-        yield_singleton PureThy.add_axioms
-        ((lub_take_bind, lub_take_eqn), []) thy;
+    val (lub_take_thm, thy) = Drule.add_axiom (lub_take_bind, lub_take_eqn) thy;
   in
     (lub_take_thm, thy)
   end;

--- a/src/Pure/axclass.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/Pure/axclass.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -521,7 +521,7 @@
     val names = name args;
   in
     thy
-    |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
+    |> fold_map Drule.add_axiom (map Binding.name names ~~ specs)
     |-> fold add
   end;
 

--- a/src/Pure/drule.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/Pure/drule.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -77,6 +77,7 @@
   val flexflex_unique: thm -> thm
   val export_without_context: thm -> thm
   val export_without_context_open: thm -> thm
+  val add_axiom: (binding * term) -> theory -> thm * theory
   val store_thm: binding -> thm -> thm
   val store_standard_thm: binding -> thm -> thm
   val store_thm_open: binding -> thm -> thm
@@ -320,6 +321,12 @@
   #> Thm.close_derivation;
 
 
+(* old-style axioms *)
+
+fun add_axiom (b, prop) =
+  Thm.add_axiom (b, prop) #-> (fn thm => PureThy.add_thm ((b, export_without_context thm), []));
+
+
 (*Convert all Vars in a theorem to Frees.  Also return a function for
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   Similar code in type/freeze_thaw*)

--- a/src/Pure/pure_thy.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/Pure/pure_thy.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -32,7 +32,6 @@
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     -> theory -> (string * thm list) list * theory
-  val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
   val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
@@ -201,18 +200,14 @@
 (* store axioms as theorems *)
 
 local
-  fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
-  fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
-  fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy =>
+  fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
     let
-      val named_ax = [(b, ax)];
-      val thy' = add named_ax thy;
-      val thm = hd (get_axs thy' named_ax);
+      val thy' = add [(b, prop)] thy;
+      val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
     in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
 in
   val add_defs               = add_axm o Theory.add_defs_i false;
   val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
-  val add_axioms             = add_axm Theory.add_axioms_i;
   val add_defs_cmd           = add_axm o Theory.add_defs false;
   val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
 end;
@@ -367,6 +362,6 @@
   #> Sign.hide_const false "Pure.sort_constraint"
   #> Sign.hide_const false "Pure.conjunction"
   #> add_thmss [((Binding.name "nothing", []), [])] #> snd
-  #> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms)));
+  #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
 
 end;