src/HOL/IMP/Abs_State.thy

--- a/src/HOL/IMP/Abs_State.thy	Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Fri Jan 27 17:02:08 2012 +0100
@@ -58,7 +58,7 @@
 lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
 by(auto simp add: le_st_def lookup_def update_def)
 
-context Val_abs
+locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
 begin
 
 abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"