--- 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);