src/HOL/IMP/Abs_State.thy

--- a/src/HOL/IMP/Abs_State.thy	Sat Apr 27 21:56:45 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Sun Apr 28 09:10:43 2013 +0200
@@ -20,6 +20,7 @@
 hide_type st  --"hide previous def to avoid long names"
 
 quotient_type 'a st = "('a::top) st_rep" / eq_st
+morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)
 
 lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"