src/HOL/Real/Hyperreal/HyperDef.thy

--- a/src/HOL/Real/Hyperreal/HyperDef.thy	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.thy	Wed Jul 19 12:33:19 2000 +0200
@@ -22,7 +22,7 @@
     "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
 
-typedef hypreal = "{x::nat=>real. True}/hyprel"   (Equiv.quotient_def)
+typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
 
 instance
    hypreal  :: {ord, zero, plus, times, minus}