src/HOL/Library/Quotient.thy

--- a/src/HOL/Library/Quotient.thy	Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/Library/Quotient.thy	Tue Jan 03 11:32:55 2006 +0100
@@ -75,7 +75,7 @@
 *}
 
 constdefs
-  class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
+  "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
 
 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"