TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;

--- a/src/Pure/General/table.ML	Thu Mar 05 14:29:02 2009 +0100
+++ b/src/Pure/General/table.ML	Thu Mar 05 15:25:35 2009 +0100
@@ -366,7 +366,7 @@
 
 fun join f (table1, table2) =
   let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
-  in fold_table add table2 table1 end;
+  in if pointer_eq (table1, table2) then table1 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);