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