# HG changeset patch
# User wenzelm
# Date 1236263135 -3600
# Node ID 520872460b7b202d9b2e28f2b267be723e3942f3
# Parent  a16af775e08d6a40692ebde8ecbda27c1f5a3138
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;

diff -r a16af775e08d -r 520872460b7b src/Pure/General/table.ML
--- 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);