| changeset 46667 | 318b669fe660 |
| parent 46665 | 919dfcdf6d8a |
| child 46668 | 9034b44844bd |
--- a/src/Pure/General/graph.ML Sat Feb 25 13:00:32 2012 +0100 +++ b/src/Pure/General/graph.ML Sat Feb 25 13:13:14 2012 +0100 @@ -319,4 +319,5 @@ end; structure Graph = Graph(type key = string val ord = fast_string_ord); +structure String_Graph = Graph(type key = string val ord = string_ord); structure Int_Graph = Graph(type key = int val ord = int_ord);