# HG changeset patch
# User wenzelm
# Date 1120564509 -7200
# Node ID 51fa05ce0f3213a852205f76a3ddab5dfb5851ff
# Parent  cc735c10b44d634cac55f7a92af266105ad617b1
Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;

diff -r cc735c10b44d -r 51fa05ce0f32 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Jul 05 13:54:20 2005 +0200
+++ b/src/Pure/General/table.ML	Tue Jul 05 13:55:09 2005 +0200
@@ -359,4 +359,4 @@
 end;
 
 structure Inttab = TableFun(type key = int val ord = int_ord);
-structure Symtab = TableFun(type key = string val ord = string_ord);
+structure Symtab = TableFun(type key = string val ord = fast_string_ord);