author | haftmann |
Wed, 19 Oct 2005 17:21:53 +0200 | |
changeset 17913 | 4159e1523ad8 |
parent 17912 | 410ec3b7e771 |
child 17914 | 99ead7a7eb42 |
--- 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 +);