src/Pure/General/set.ML
changeset 77805 66779a752f10
parent 77802 25c114e2528e
child 77813 622ba814e01c
equal deleted inserted replaced
77804:849c996f052b 77805:66779a752f10
   443 val fold_rev = fold_rev_set;
   443 val fold_rev = fold_rev_set;
   444 
   444 
   445 end;
   445 end;
   446 
   446 
   447 structure Intset = Set(Inttab.Key);
   447 structure Intset = Set(Inttab.Key);
       
   448 structure Intset' = Set(Inttab'.Key);
   448 structure Symset = Set(Symtab.Key);
   449 structure Symset = Set(Symtab.Key);