diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/PER.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -153,7 +153,7 @@
 
 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
 
-typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
+typedef 'a quot = "quot :: 'a::partial_equiv set set"
   unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"