src/HOL/IMP/Abs_Int1_parity.thy

--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Apr 04 22:46:14 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Apr 05 15:13:25 2013 +0200
@@ -53,7 +53,7 @@
 begin
 
 definition sup_parity where
-"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
+"x \<squnion> y = (if x = y then x else Either)"
 
 definition top_parity where
 "\<top> = Either"