tuned

--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 04:20:42 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 04:30:05 2013 +0200
@@ -27,9 +27,7 @@
 
 definition "x < (y::const) = (x \<le> y & \<not> y \<le> x)"
 
-fun sup_const where
-"Const i \<squnion> Const j = (if i=j then Const i else Any)" |
-"_ \<squnion> _ = Any"
+fun sup_const where "x \<squnion> y = (if x=y then x else Any)"
 
 definition "\<top> = Any"