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