# HG changeset patch
# User wenzelm
# Date 1394559377 -3600
# Node ID d1130b831e93c7fafe5649d3f61046a459699686
# Parent  030531cc4c62999f07722da5aba80d0f79b9b882
more standard internal data integrity;

diff -r 030531cc4c62 -r d1130b831e93 src/Pure/General/change_table.ML
--- a/src/Pure/General/change_table.ML	Tue Mar 11 18:26:47 2014 +0100
+++ b/src/Pure/General/change_table.ML	Tue Mar 11 18:36:17 2014 +0100
@@ -15,6 +15,7 @@
   type 'a T
   val table_of: 'a T -> 'a Table.table
   val empty: 'a T
+  val is_empty: 'a T -> bool
   val change_base: bool -> 'a T -> 'a T
   val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T  (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T  (*exception DUP*)
@@ -79,7 +80,9 @@
 datatype 'a T = Change_Table of {change: change option, table: 'a Table.table};
 
 fun table_of (Change_Table {table, ...}) = table;
+
 val empty = Change_Table {change = NONE, table = Table.empty};
+fun is_empty (Change_Table {change, table}) = is_none change andalso Table.is_empty table;
 
 fun make_change_table (change, table) = Change_Table {change = change, table = table};
 fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
@@ -94,8 +97,9 @@
     val Change_Table {change = change1, table = table1} = arg1;
     val Change_Table {change = change2, table = table2} = arg2;
   in
-    if pointer_eq (table1, table2) orelse Table.is_empty table2 then arg1
-    else if Table.is_empty table1 then arg2
+    if pointer_eq (change1, change2) andalso pointer_eq (table1, table2) then arg1
+    else if is_empty arg2 then arg1
+    else if is_empty arg1 then arg2
     else
       (case merge_change (change1, change2) of
         NONE => make_change_table (NONE, Table.join f (table1, table2))