src/HOL/Real/PReal.thy

--- a/src/HOL/Real/PReal.thy	Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Oct 11 10:52:51 1999 +0200
@@ -9,7 +9,7 @@
 
 PReal = PRat +
 
-typedef preal = "{A::prat set. {} < A & A < {q::prat. True} &
+typedef preal = "{A::prat set. {} < A & A < UNIV &
                                (!y: A. ((!z. z < y --> z: A) &
                                         (? u: A. y < u)))}"      (preal_1)
 instance