# HG changeset patch
# User haftmann
# Date 1130484904 -7200
# Node ID 2c9005459d15104a39c1cb334504ad21dd980b7f
# Parent  535de280c812215f7002b31f97d92ae0fa939530
removed obfuscating PStrStrTab

diff -r 535de280c812 -r 2c9005459d15 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Oct 28 08:40:55 2005 +0200
+++ b/src/Pure/General/table.ML	Fri Oct 28 09:35:04 2005 +0200
@@ -389,7 +389,3 @@
 
 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
-);