# HG changeset patch
# User wenzelm
# Date 1681143393 -7200
# Node ID 66779a752f10d53b02f299da80686ab363adce6c
# Parent  849c996f052b2aa0a34514fac5f0519e1f3c67d3
more Set() and Table() instances;

diff -r 849c996f052b -r 66779a752f10 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Mon Apr 10 18:13:23 2023 +0200
+++ b/src/Pure/General/set.ML	Mon Apr 10 18:16:33 2023 +0200
@@ -445,4 +445,5 @@
 end;
 
 structure Intset = Set(Inttab.Key);
+structure Intset' = Set(Inttab'.Key);
 structure Symset = Set(Symtab.Key);
diff -r 849c996f052b -r 66779a752f10 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Apr 10 18:13:23 2023 +0200
+++ b/src/Pure/General/table.ML	Mon Apr 10 18:16:33 2023 +0200
@@ -645,6 +645,7 @@
 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);