# HG changeset patch
# User haftmann
# Date 1140019746 -3600
# Node ID 88d25a6c346a28d29c0b307ea087939dc7195596
# Parent  8eae46249628fbc216cee211ecdf725b42910723
exported specifications_of

diff -r 8eae46249628 -r 88d25a6c346a src/Pure/defs.ML
--- 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 *)