changeset 17913 | 4159e1523ad8 |
parent 17709 | 299eeb303f04 |
child 18007 | 2c9005459d15 |
--- a/src/Pure/General/table.ML Wed Oct 19 17:19:52 2005 +0200 +++ b/src/Pure/General/table.ML Wed Oct 19 17:21:53 2005 +0200 @@ -389,3 +389,7 @@ structure Inttab = TableFun(type key = int val ord = int_ord); structure Symtab = TableFun(type key = string val ord = fast_string_ord); +structure PStrStrTab = TableFun( + type key = string * string + val ord = prod_ord fast_string_ord fast_string_ord +);