# HG changeset patch
# User wenzelm
# Date 1393267449 -3600
# Node ID 7e330ae052bb6df8f8bea634a28d1335581b16e2
# Parent  945ad7eaf37f82e32ea876ef15ffc3f31d4a6044
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);

diff -r 945ad7eaf37f -r 7e330ae052bb src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Feb 24 19:33:39 2014 +0100
+++ b/src/Pure/General/table.ML	Mon Feb 24 19:44:09 2014 +0100
@@ -368,8 +368,13 @@
 fun make entries = fold update_new entries empty;
 
 fun join f (table1, table2) =
-  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 fold_table add table2 table1 end;
+  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
+  end;
 
 fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);