src/Pure/defs.ML
changeset 19050 527bc006f2b6
parent 19040 88d25a6c346a
child 19135 2de31ba562d7
     1.1 --- a/src/Pure/defs.ML	Wed Feb 15 21:34:59 2006 +0100
     1.2 +++ b/src/Pure/defs.ML	Wed Feb 15 21:35:00 2006 +0100
     1.3 @@ -65,8 +65,9 @@
     1.4          (check_specified c spec specs; Inttab.update spec specs));
     1.5    in (consts', specified') end);
     1.6  
     1.7 -fun specifications_of (Defs { specified, ... }) c =
     1.8 -  (map (snd o snd) o Inttab.dest o the o Symtab.lookup specified) c;
     1.9 +fun specifications_of (Defs {specified, ...}) c =
    1.10 +  (map (snd o snd) o Inttab.dest o the_default Inttab.empty o Symtab.lookup specified) c;
    1.11 +
    1.12  
    1.13  (* empty and merge *)
    1.14