src/Pure/defs.ML

       |> Symtab.map_entry c (fn specs =>
         (check_specified c spec specs; Inttab.update spec specs));
   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;