src/Pure/sorts.ML

     val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
     fun restrict_arity tyco (c, (_, Ss)) =
       if P c then case sargs (c, tyco)
        of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
           |> map restrict_sort))
+        | NONE => NONE
       else NONE;
     val classes' = classes |> Graph.subgraph P;
     val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
   in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;