| author | wenzelm |
| Wed, 13 Jul 2005 16:07:32 +0200 | |
| changeset 16810 | 2406588f99cb |
| parent 16809 | 8ca51a846576 |
| child 16811 | 23b9c52612db |
--- 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);