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