optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);

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