src/Pure/defs.ML

--- a/src/Pure/defs.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/defs.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -69,7 +69,7 @@
   in (consts', specified') end);
 
 fun specifications_of (Defs {specified, ...}) c =
-  (List.mapPartial
+  (map_filter
     (fn (_, (false, _, _, _)) => NONE
       | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest
     o the_default Inttab.empty o Symtab.lookup specified) c;