# HG changeset patch
# User haftmann
# Date 1129735313 -7200
# Node ID 4159e1523ad82878ec5c8be07d705cd9e27e91f9
# Parent  410ec3b7e771b4b222d238d86bf1410b719fd577
added table functor instance for pairs of strings

diff -r 410ec3b7e771 -r 4159e1523ad8 src/Pure/General/table.ML
--- 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
+);