src/HOL/IMP/Abs_Int1_const.thy

--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Apr 30 03:18:07 2013 +0200
@@ -20,7 +20,7 @@
   (case (a1,a2) of (Const i, Const j) \<Rightarrow> Const(i+j) | _ \<Rightarrow> Any)"
 by(auto split: prod.split const.split)
 
-instantiation const :: semilattice
+instantiation const :: semilattice_sup_top
 begin
 
 fun less_eq_const where "x \<le> y = (y = Any | x=y)"