src/Pure/drule.ML
changeset 35897 8758895ea413
parent 35856 f81557a124d5
child 35985 0bbf0d2348f9
--- 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*)