changeset 17913 | 4159e1523ad8 |
parent 17709 | 299eeb303f04 |
child 18007 | 2c9005459d15 |
17912:410ec3b7e771 | 17913:4159e1523ad8 |
---|---|
387 |
387 |
388 end; |
388 end; |
389 |
389 |
390 structure Inttab = TableFun(type key = int val ord = int_ord); |
390 structure Inttab = TableFun(type key = int val ord = int_ord); |
391 structure Symtab = TableFun(type key = string val ord = fast_string_ord); |
391 structure Symtab = TableFun(type key = string val ord = fast_string_ord); |
392 structure PStrStrTab = TableFun( |
|
393 type key = string * string |
|
394 val ord = prod_ord fast_string_ord fast_string_ord |
|
395 ); |