# HG changeset patch
# User aspinall
# Date 1170159418 -3600
# Node ID ac81ad3436bcdaa8c86afb8a4c17cda53d8d287d
# Parent  6e9ab159512f33f675ae77c8adbf2dcda6a6d26c
Add get_succs

diff -r 6e9ab159512f -r ac81ad3436bc src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jan 30 13:14:41 2007 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Jan 30 13:16:58 2007 +0100
@@ -34,6 +34,7 @@
   val get_theory: string -> theory
   val the_theory: string -> theory -> theory
   val get_preds: string -> string list
+  val get_succs: string -> string list
   val loaded_files: string -> Path.T list
   val touch_child_thys: string -> unit
   val touch_all_thys: unit -> unit
@@ -237,6 +238,10 @@
 fun touch_thy name = touch_thys [name];
 fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
 
+fun get_succs name =
+  (thy_graph Graph.imm_succs name) handle Graph.UNDEF _ =>
+    error (loader_msg "nothing known about theory" [name]);
+
 fun touch_all_thys () = List.app outdate_thy (get_names ());
 
 end;