diff -r 13863eaf372a -r aece9a063271 src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Fri Jun 30 16:26:03 2023 +0200 +++ b/src/Pure/General/graph.scala Sat Jul 01 16:27:34 2023 +0200 @@ -66,7 +66,16 @@ } -final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) { +final class Graph[Key, A] private( + protected val rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))] +) { + override def hashCode: Int = rep.hashCode + override def equals(that: Any): Boolean = + that match { + case other: Graph[_, _] => rep == other.rep + case _ => false + } + type Keys = SortedSet[Key] type Entry = (A, (Keys, Keys))