Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;
authorwenzelm
Tue, 05 Jul 2005 13:55:09 +0200
changeset 16687 51fa05ce0f32
parent 16686 cc735c10b44d
child 16688 e3de7ea24c23
Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;
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);