src/HOL/Prod.thy

--- a/src/HOL/Prod.thy	Thu Apr 03 10:36:54 1997 +0200
+++ b/src/HOL/Prod.thy	Thu Apr 03 19:29:53 1997 +0200
@@ -79,7 +79,7 @@
 
 (** unit **)
 
-typedef  unit = "{p. p = True}"
+typedef  unit = "{True}"
 
 consts
   "()"          :: unit                           ("'(')")