src/Pure/defs.ML
changeset 19482 9f11af8f7ef9
parent 19339 59f08f67ed3f
child 19569 1c23356a8ea8
     1.1 --- a/src/Pure/defs.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    in (consts', specified') end);
     1.5  
     1.6  fun specifications_of (Defs {specified, ...}) c =
     1.7 -  (List.mapPartial
     1.8 +  (map_filter
     1.9      (fn (_, (false, _, _, _)) => NONE
    1.10        | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest
    1.11      o the_default Inttab.empty o Symtab.lookup specified) c;