Add get_succs
authoraspinall
Tue, 30 Jan 2007 13:16:58 +0100
changeset 22215 ac81ad3436bc
parent 22214 6e9ab159512f
child 22216 c3f5aa951a68
Add get_succs
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;