--- a/src/Pure/General/graph.ML Tue Feb 07 19:56:51 2006 +0100
+++ b/src/Pure/General/graph.ML Tue Feb 07 19:56:53 2006 +0100
@@ -53,7 +53,7 @@
type key = Key.key;
-val eq_key = equal EQUAL o Key.ord;
+val eq_key = is_equal o Key.ord;
val member_key = member eq_key;
val remove_key = remove eq_key;