diff -r 8ca51a846576 -r 2406588f99cb src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Jul 13 16:07:30 2005 +0200
+++ b/src/Pure/General/graph.ML	Wed Jul 13 16:07:32 2005 +0200
@@ -214,4 +214,4 @@
 
 
 (*graphs indexed by strings*)
-structure Graph = GraphFun(type key = string val ord = string_ord);
+structure Graph = GraphFun(type key = string val ord = fast_string_ord);