unused (see also 864c7c684651 and b6aa5eac0a1a);
authorwenzelm
Wed, 19 Apr 2023 11:10:52 +0200
changeset 77881 560bdb9f2101
parent 77880 41f1fd0fdb80
child 77882 bb7238e7d2d9
unused (see also 864c7c684651 and b6aa5eac0a1a);
src/Pure/General/set.ML
src/Pure/General/table.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);
--- 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);