more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy");

--- a/src/Pure/term_items.ML	Wed Dec 20 12:50:38 2023 +0100
+++ b/src/Pure/term_items.ML	Wed Dec 20 14:26:18 2023 +0100
@@ -28,12 +28,12 @@
   val defined: 'a table -> key -> bool
   val update: key * 'a -> 'a table -> 'a table
   val remove: key -> 'a table -> 'a table
+  val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
   val add: key * 'a -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table
   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  (*exception DUP*)
   val unsynchronized_cache: (key -> 'a) -> key -> 'a
   type set = int table
   val add_set: key -> set -> set
@@ -78,6 +78,7 @@
 
 fun update e (Table tab) = Table (Table.update e tab);
 fun remove x (Table tab) = Table (Table.delete_safe x tab);
+fun insert eq e (Table tab) = Table (Table.insert eq e tab);
 
 fun add entry (Table tab) = Table (Table.default entry tab);
 fun make es = build (fold add es);
@@ -85,8 +86,6 @@
 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);
-
 val unsynchronized_cache = Table.unsynchronized_cache;
 
 

--- a/src/Pure/zterm.ML	Wed Dec 20 12:50:38 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 20 14:26:18 2023 +0100
@@ -466,7 +466,8 @@
 exception BAD_INST of ((indexname * ztyp) * zterm) list
 
 fun make_inst inst =
-  ZVars.make_strict inst handle ZVars.DUP _ => raise BAD_INST inst;
+  ZVars.build (inst |> fold (ZVars.insert (op aconv_zterm)))
+    handle ZVars.DUP _ => raise BAD_INST inst;
 
 fun map_insts_same typ term (instT, inst) =
   let