diff -r 63fb7a68a12c -r 1efe2f3728a6 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Tue Oct 13 17:27:11 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Tue Oct 13 19:22:25 2015 +0200
@@ -18,8 +18,9 @@
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
 hide_type st  --"hide previous def to avoid long names"
+declare [[typedef_overloaded]] --"allow quotient types to depend on classes"
 
-quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
+quotient_type 'a st = "('a::top) st_rep" / eq_st
 morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)