# HG changeset patch
# User wenzelm
# Date 1001622178 -7200
# Node ID bf6700f4c0102c949c57e816d8b2517bb663c3fb
# Parent  9273cef990f5fb8fb44fa68a6d51ac78e29f0b04
renamed "()" to Unity, made local;

diff -r 9273cef990f5 -r bf6700f4c010 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Sep 27 22:22:08 2001 +0200
+++ b/src/HOL/Product_Type.thy	Thu Sep 27 22:22:58 2001 +0200
@@ -96,21 +96,15 @@
 
 (** unit **)
 
-global
-
 typedef unit = "{True}"
 proof
   show "True : ?unit"
     by blast
 qed
 
-consts
-  "()"          :: unit                           ("'(')")
-
-local
-
-defs
-  Unity_def:    "() == Abs_unit True"
+constdefs
+  Unity :: unit    ("'(')")
+  "() == Abs_unit True"