Library.is_equal;
authorwenzelm
Tue, 07 Feb 2006 19:56:53 +0100
changeset 18970 d055a29ddd23
parent 18969 49aa2c8791ba
child 18971 f95650f3b5bf
Library.is_equal;
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;