--- a/src/Pure/term_items.ML Wed Dec 06 13:04:07 2023 +0100
+++ b/src/Pure/term_items.ML Wed Dec 06 13:16:34 2023 +0100
@@ -32,6 +32,7 @@
val make1: key * 'a -> 'a table
val make2: key * 'a -> key * 'a -> 'a table
val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
+ val make_strict: (key * 'a) list -> 'a table
type set = int table
val add_set: key -> set -> set
val make_set: key list -> set
@@ -81,6 +82,8 @@
fun make2 e1 e2 = build (add e1 #> add e2);
fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
+fun make_strict es = Table (Table.make es);
+
(* set with order of addition *)