diff -r 56adbf5bcc82 -r f8f788c8b7f3 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:34:50 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Jan 16 12:33:26 2012 +0100
@@ -27,7 +27,7 @@
 val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
 val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
 
-(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
+(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
 fun typedef_term rel rty lthy =
   let
     val [x, c] =