| changeset 16810 | 2406588f99cb |
| parent 16445 | bc90e58bb6ac |
| child 16894 | 40f80823b451 |
--- 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);