src/Pure/General/table.ML
changeset 17913 4159e1523ad8
parent 17709 299eeb303f04
child 18007 2c9005459d15
equal deleted inserted replaced
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 );