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