# HG changeset patch
# User nipkow
# Date 860088593 -7200
# Node ID fd5645efa43d1c057d340b0f42428eadbc0412f6
# Parent  8d229dc0cfe2755b09671e5d8e6ada6068a8fa93
Now: unit = {True}

diff -r 8d229dc0cfe2 -r fd5645efa43d src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Apr 03 10:36:54 1997 +0200
+++ b/src/HOL/Prod.ML	Thu Apr 03 19:29:53 1997 +0200
@@ -302,7 +302,7 @@
 
 goalw Prod.thy [Unity_def]
     "u = ()";
-by (stac (rewrite_rule [unit_def] Rep_unit RS CollectD RS sym) 1);
+by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
 by (rtac (Rep_unit_inverse RS sym) 1);
 qed "unit_eq";
  
diff -r 8d229dc0cfe2 -r fd5645efa43d 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                           ("'(')")