# HG changeset patch
# User wenzelm
# Date 1701259557 -3600
# Node ID 6b071d4041d59b5e405da605254e1d668f87b877
# Parent  a1b5357b547335676929e4f133ff86835565076f
tuned signature;

diff -r a1b5357b5473 -r 6b071d4041d5 src/Pure/General/bitset.ML
--- a/src/Pure/General/bitset.ML	Wed Nov 29 13:01:03 2023 +0100
+++ b/src/Pure/General/bitset.ML	Wed Nov 29 13:05:57 2023 +0100
@@ -9,6 +9,8 @@
 sig
   structure Key: KEY
   type elem
+  val make_elem: int * int -> elem  (*exception*)
+  val dest_elem: elem -> int * int
   type T
   val empty: T
   val build: (T -> T) -> T
@@ -80,7 +82,7 @@
 structure Key = Inttab.Key;
 type elem = Key.key;
 
-fun make_elem m n : elem = if check_bit n then m * word_size + n else raise BAD n;
+fun make_elem (m, n) : elem = if check_bit n then m * word_size + n else raise BAD n;
 fun dest_elem (x: elem) = Integer.div_mod x word_size;
 
 datatype T = Bitset of word Inttab.table;
@@ -99,11 +101,11 @@
 
 fun fold_set f (Bitset t) =
   Inttab.fold (fn (m, w) =>
-    (if m < 0 then fold_rev_bits else fold_bits) (f o make_elem m) w) t;
+    (if m < 0 then fold_rev_bits else fold_bits) (fn n => f (make_elem (m, n))) w) t;
 
 fun fold_rev_set f (Bitset t) =
   Inttab.fold_rev (fn (m, w) =>
-    (if m < 0 then fold_bits else fold_rev_bits) (f o make_elem m) w) t;
+    (if m < 0 then fold_bits else fold_rev_bits) (fn n => f (make_elem (m, n))) w) t;
 
 val dest = Library.build o fold_rev_set cons;
 
@@ -112,11 +114,11 @@
 
 fun min (Bitset t) =
   Inttab.min t |> Option.map (fn (m, w) =>
-    make_elem m (fold_bits Integer.min w max_bit));
+    make_elem (m, fold_bits Integer.min w max_bit));
 
 fun max (Bitset t) =
   Inttab.max t |> Option.map (fn (m, w) =>
-    make_elem m (fold_bits Integer.max w min_bit));
+    make_elem (m, fold_bits Integer.max w min_bit));
 
 
 (* linear search *)