--- 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*)