# HG changeset patch
# User nipkow
# Date 1367133043 -7200
# Node ID 674522b0d06d4fca62de4597b99d0d95c42f15f5
# Parent  8fcf6e32544e1e2ce7f3297f8fade55d55a3c440
tuned

diff -r 8fcf6e32544e -r 674522b0d06d 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"