src/Pure/defs.ML

--- a/src/Pure/defs.ML	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Pure/defs.ML	Thu Sep 24 13:33:42 2015 +0200
@@ -12,6 +12,7 @@
   val item_ord: item * item -> order
   type entry = item * typ list
   val pretty_args: Proof.context -> typ list -> Pretty.T list
+  val pretty_entry: Proof.context -> entry -> Pretty.T
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -28,6 +29,7 @@
   val empty: T
   val merge: Proof.context -> T * T -> T
   val define: Proof.context -> bool -> string option -> string -> entry -> entry list -> T -> T
+  val get_deps: T -> item -> (typ list * entry list) list
 end;
 
 structure Defs: DEFS =
@@ -241,4 +243,6 @@
     val defs' = defs |> update_specs c spec;
   in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
 
+fun get_deps (Defs defs) c = reducts_of defs c;
+
 end;