# HG changeset patch
# User nipkow
# Date 1444756945 -7200
# Node ID 1efe2f3728a67f947b569218dacfe647b750e231
# Parent  63fb7a68a12cccdc3bd947d7619a6738943b541a
prefer undecorated typedef

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)