Added function get_preds.
authorberghofe
Mon, 17 May 1999 17:07:54 +0200
changeset 6654 c3686d75e9d6
parent 6653 b0b819902eaa
child 6655 c151515d4efa
Added function get_preds.
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 *)