Added function get_preds.
--- 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 *)