src/Pure/General/set.ML
changeset 77805 66779a752f10
parent 77802 25c114e2528e
child 77813 622ba814e01c
--- 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);