# HG changeset patch
# User haftmann
# Date 1237719382 -3600
# Node ID ef8f46c3158a31fee2819d79c718ac01873c6e26
# Parent  bc3c1b7df4ec830f5fb7880518a9b7c093b66a14
added Symreltab (binary relations of symbols) instance of TableFun

diff -r bc3c1b7df4ec -r ef8f46c3158a src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Mar 21 20:39:38 2009 +0100
+++ b/src/Pure/General/table.ML	Sun Mar 22 11:56:22 2009 +0100
@@ -383,3 +383,6 @@
 
 structure Inttab = TableFun(type key = int val ord = int_ord);
 structure Symtab = TableFun(type key = string val ord = fast_string_ord);
+structure Symreltab = TableFun(type key = string * string
+  val ord = prod_ord fast_string_ord fast_string_ord);
+