diff -r d1641dba61e5 -r 21dbff595bf6 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jul 07 18:38:00 2005 +0200
+++ b/src/Pure/theory.ML	Thu Jul 07 19:01:04 2005 +0200
@@ -38,6 +38,7 @@
   val oracle_space: theory -> NameSpace.T
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
+  val defs_of : theory -> Defs.graph
   val self_ref: theory -> theory_ref
   val deref: theory_ref -> theory
   val merge: theory * theory -> theory                     (*exception TERM*)
@@ -178,6 +179,8 @@
 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
 fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
 
+fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D)
+
 fun requires thy name what =
   if Context.exists_name name thy then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);