--- a/src/Pure/defs.ML Tue Feb 14 17:07:48 2006 +0100
+++ b/src/Pure/defs.ML Wed Feb 15 17:09:06 2006 +0100
@@ -11,6 +11,7 @@
type T
val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
val empty: T
+ val specifications_of: T -> string -> typ list
val merge: Pretty.pp -> T * T -> T
end
@@ -64,6 +65,8 @@
(check_specified c spec specs; Inttab.update spec specs));
in (consts', specified') end);
+fun specifications_of (Defs { specified, ... }) c =
+ (map (snd o snd) o Inttab.dest o the o Symtab.lookup specified) c;
(* empty and merge *)