# HG changeset patch
# User wenzelm
# Date 1394656186 -3600
# Node ID f74d0a4d8ae389c8ae37641404c3ab7b97716521
# Parent  5c2435c79415ff8e4df1b193dc275b4403826414
proper base comparison;

diff -r 5c2435c79415 -r f74d0a4d8ae3 src/Pure/General/change_table.ML
--- a/src/Pure/General/change_table.ML	Wed Mar 12 21:28:09 2014 +0100
+++ b/src/Pure/General/change_table.ML	Wed Mar 12 21:29:46 2014 +0100
@@ -68,7 +68,7 @@
         val {base = base1, depth = depth1, changes = changes1} = change1;
         val {base = base2, depth = depth2, changes = changes2} = change2;
       in
-        if base1 = base1 andalso depth1 = depth2 then
+        if base1 = base2 andalso depth1 = depth2 then
           SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
         else cannot_merge ()
       end