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