# HG changeset patch
# User wenzelm
# Date 1680549392 -7200
# Node ID c55c4c0c9ef945c3efcc695b3965c66dbed3fe88
# Parent  97febdb6ee5856d804b128a68b2eee277317a1c1
tuned;

diff -r 97febdb6ee58 -r c55c4c0c9ef9 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Apr 03 21:13:46 2023 +0200
+++ b/src/Pure/General/table.ML	Mon Apr 03 21:16:32 2023 +0200
@@ -546,13 +546,13 @@
 
 fun make entries = build (fold update_new entries);
 
-fun join f (table1, table2) =
+fun join f (tab1, tab2) =
   let
     fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
   in
-    if pointer_eq (table1, table2) then table1
-    else if is_empty table1 then table2
-    else fold_table add table2 table1
+    if pointer_eq (tab1, tab2) then tab1
+    else if is_empty tab1 then tab2
+    else fold_table add tab2 tab1
   end;
 
 fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);