src/Pure/sorts.ML
changeset 46614 165886a4fe64
parent 45595 fe57d786fd5b
child 47005 421760a1efe7
--- a/src/Pure/sorts.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Pure/sorts.ML	Thu Feb 23 15:49:40 2012 +0100
@@ -308,7 +308,7 @@
             SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
         | NONE => NONE)
       else NONE;
-    val classes' = classes |> Graph.subgraph P;
+    val classes' = classes |> Graph.restrict P;
     val arities' = arities |> Symtab.map (map_filter o restrict_arity);
   in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;