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