# HG changeset patch
# User wenzelm
# Date 1269282551 -3600
# Node ID 8758895ea4136b0cdae6496c53a605740ca194f3
# Parent  487b267433b1d2cb1a84aa1018c90f1af3c5323e
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;

diff -r 487b267433b1 -r 8758895ea413 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 22 19:26:12 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 22 19:29:11 2010 +0100
@@ -177,10 +177,10 @@
          val new_defs = map new_def assms
          val (definition, thy') = thy
           |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> fold_map Drule.add_axiom (map_index
-              (fn (i, t) => (Binding.name (constname ^ "_def" ^ string_of_int i), t)) new_defs)
+          |> fold_map Specification.axiom (map_index
+              (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
         in
-          (lhs, ((full_constname, definition) :: defs, thy'))
+          (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
         end
       else
         (atom, (defs, thy)))
diff -r 487b267433b1 -r 8758895ea413 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Mon Mar 22 19:26:12 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Mon Mar 22 19:29:11 2010 +0100
@@ -44,9 +44,10 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thm, thy') = Drule.add_axiom (Binding.name axname, HOLogic.mk_Trueprop tm) thy
+                    val (thm, thy') =
+                      Specification.axiom ((Binding.name axname, []), HOLogic.mk_Trueprop tm) thy
                 in
-                    (thy', thm)
+                    (thy', Drule.export_without_context thm)
                 end
               | process ((thname,cname,covld)::cos) (thy,tm) =
                 case tm of
diff -r 487b267433b1 -r 8758895ea413 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 22 19:26:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 22 19:29:11 2010 +0100
@@ -54,8 +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) = 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 (abs_iso_thm, thy) = Specification.axiom ((abs_iso_bind, []), abs_iso_eqn) thy;
+    val (rep_iso_thm, thy) = Specification.axiom ((rep_iso_bind, []), rep_iso_eqn) thy;
 
     val result =
         {
@@ -63,8 +63,8 @@
           repT = rhsT,
           abs_const = abs_const,
           rep_const = rep_const,
-          abs_inverse = abs_iso_thm,
-          rep_inverse = rep_iso_thm
+          abs_inverse = Drule.export_without_context abs_iso_thm,
+          rep_inverse = Drule.export_without_context rep_iso_thm
         };
   in
     (result, thy)
@@ -83,9 +83,9 @@
 
     val lub_take_bind = Binding.qualified true "lub_take" dbind;
 
-    val (lub_take_thm, thy) = Drule.add_axiom (lub_take_bind, lub_take_eqn) thy;
+    val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy;
   in
-    (lub_take_thm, thy)
+    (Drule.export_without_context lub_take_thm, thy)
   end;
 
 fun add_axioms
diff -r 487b267433b1 -r 8758895ea413 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Mar 22 19:26:12 2010 +0100
+++ b/src/Pure/drule.ML	Mon Mar 22 19:29:11 2010 +0100
@@ -77,7 +77,6 @@
   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
@@ -321,12 +320,6 @@
   #> 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*)