src/Pure/defs.ML
changeset 19040 88d25a6c346a
parent 19025 596fb1eb7856
child 19050 527bc006f2b6
     1.1 --- a/src/Pure/defs.ML	Tue Feb 14 17:07:48 2006 +0100
     1.2 +++ b/src/Pure/defs.ML	Wed Feb 15 17:09:06 2006 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4    type T
     1.5    val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
     1.6    val empty: T
     1.7 +  val specifications_of: T -> string -> typ list
     1.8    val merge: Pretty.pp -> T * T -> T
     1.9  end
    1.10  
    1.11 @@ -64,6 +65,8 @@
    1.12          (check_specified c spec specs; Inttab.update spec specs));
    1.13    in (consts', specified') end);
    1.14  
    1.15 +fun specifications_of (Defs { specified, ... }) c =
    1.16 +  (map (snd o snd) o Inttab.dest o the o Symtab.lookup specified) c;
    1.17  
    1.18  (* empty and merge *)
    1.19