# HG changeset patch
# User wenzelm
# Date 1139338613 -3600
# Node ID d055a29ddd23a60d3c4e59ea74bfb4b153e30683
# Parent  49aa2c8791baf83c608f69cf66572dc97b15f70c
Library.is_equal;

diff -r 49aa2c8791ba -r d055a29ddd23 src/Pure/General/graph.ML
--- 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;