diff -r 6dc3d5d50e57 -r e6f03fae14d5 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -19,7 +19,7 @@
 
 hide_type st  --"hide previous def to avoid long names"
 
-quotient_type 'a st = "('a::top) st_rep" / eq_st
+quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
 morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)