# HG changeset patch
# User wenzelm
# Date 1683323294 -7200
# Node ID ab6e4085a19da9ead588442d7d5cf3f3e855c407
# Parent  305a6902abb3c8562feca4cae09726770a12f797
minor performance tuning;

diff -r 305a6902abb3 -r ab6e4085a19d src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri May 05 23:03:48 2023 +0200
+++ b/src/Pure/General/table.ML	Fri May 05 23:48:14 2023 +0200
@@ -634,7 +634,8 @@
 
 fun make_list args = build (fold_rev cons_list args);
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
-fun merge_list eq = join (fn _ => Library.merge eq);
+fun merge_list eq =
+  join (fn _ => fn args => if eq_list eq args then raise SAME else Library.merge eq args);
 
 
 (* set operations *)