# HG changeset patch
# User wenzelm
# Date 1121263652 -7200
# Node ID 2406588f99cb1a030b3c92374cd4ddec25024a06
# Parent  8ca51a846576441e71d46802da7fa2904d9ca064
Graph: fast_string_ord;

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);