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;