# HG changeset patch
# User wenzelm
# Date 1681895452 -7200
# Node ID 560bdb9f2101844a5e7e947ec3e403cc9c044d2e
# Parent  41f1fd0fdb80a62158f6c00d9dd5bef96508f94c
unused (see also 864c7c684651 and b6aa5eac0a1a);

diff -r 41f1fd0fdb80 -r 560bdb9f2101 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Wed Apr 19 11:10:30 2023 +0200
+++ b/src/Pure/General/set.ML	Wed Apr 19 11:10:52 2023 +0200
@@ -464,5 +464,4 @@
 end;
 
 structure Intset = Set(Inttab.Key);
-structure Intset' = Set(Inttab'.Key);
 structure Symset = Set(Symtab.Key);
diff -r 41f1fd0fdb80 -r 560bdb9f2101 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Apr 19 11:10:30 2023 +0200
+++ b/src/Pure/General/table.ML	Wed Apr 19 11:10:52 2023 +0200
@@ -649,7 +649,6 @@
 end;
 
 structure Inttab = Table(type key = int val ord = int_ord);
-structure Inttab' = Table(type key = int val ord = rev_order o int_ord);
 structure Symtab = Table(type key = string val ord = fast_string_ord);
 structure Symreltab = Table(type key = string * string
   val ord = prod_ord fast_string_ord fast_string_ord);