diff -r 750b63fa4c4e -r 52cd8bebc3b6 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Jul 03 16:07:00 2013 +0200
@@ -148,7 +148,7 @@
 
 text{* The interface for abstract values: *}
 
-locale Val_abs =
+locale Val_semilattice =
 fixes \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
   assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
   and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
@@ -163,7 +163,7 @@
 the name of the type parameter @{typ 'av} which would otherwise be renamed to
 @{typ 'a}. *}
 
-locale Abs_Int_fun = Val_abs where \<gamma>=\<gamma>
+locale Abs_Int_fun = Val_semilattice where \<gamma>=\<gamma>
   for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
 begin