src/Pure/drule.ML
changeset 30342 d32daa6aba3c
parent 29579 cb520b766e00
child 30553 0709fda91b06
--- a/src/Pure/drule.ML	Sat Mar 07 21:57:36 2009 +0100
+++ b/src/Pure/drule.ML	Sat Mar 07 22:04:59 2009 +0100
@@ -77,6 +77,7 @@
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val flexflex_unique: thm -> thm
+  val get_def: theory -> xstring -> thm
   val store_thm: bstring -> thm -> thm
   val store_standard_thm: bstring -> thm -> thm
   val store_thm_open: bstring -> thm -> thm
@@ -459,6 +460,8 @@
 
 val read_prop = certify o SimpleSyntax.read_prop;
 
+fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
+
 fun store_thm name th =
   Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));