# HG changeset patch
# User berghofe
# Date 926953674 -7200
# Node ID c3686d75e9d6e1fefe0758456b3ab47bbf7f8cab
# Parent  b0b819902eaa4884bd6eaf0902541fd4371cd0f5
Added function get_preds.

diff -r b0b819902eaa -r c3686d75e9d6 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon May 17 17:06:50 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 17 17:07:54 1999 +0200
@@ -35,6 +35,7 @@
   val names: unit -> string list
   val get_theory: string -> theory
   val put_theory: theory -> unit
+  val get_preds: string -> string list
   val loaded_files: string -> (Path.T * File.info) list
   val load_file: bool -> Path.T -> unit
   val use_path: Path.T -> unit
@@ -123,6 +124,10 @@
 fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
 val loaded_files = mapfilter #2 o get_files;
 
+fun get_preds name =
+  (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ =>
+    error (loader_msg "nothing known about theory" [name]);
+
 
 (* access theory *)