# HG changeset patch
# User wenzelm
# Date 1001622220 -7200
# Node ID 14b03d1463d418a99da5b9dcd494ae5282c1c546
# Parent  c3724decadefdd0780d61d8b98a83e8682ff1d80
made unit type local;

diff -r c3724decadef -r 14b03d1463d4 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Thu Sep 27 22:23:20 2001 +0200
+++ b/src/HOL/hologic.ML	Thu Sep 27 22:23:40 2001 +0200
@@ -169,14 +169,14 @@
 
 (* unit *)
 
-val unitT = Type ("unit", []);
+val unitT = Type ("Product_Type.unit", []);
 
-fun is_unitT (Type ("unit", [])) = true
+fun is_unitT (Type ("Product_Type.unit", [])) = true
   | is_unitT _ = false;
 
-val unit = Const ("()", unitT);
+val unit = Const ("Product_Type.Unity", unitT);
 
-fun is_unit (Const ("()", _)) = true
+fun is_unit (Const ("Product_Type.Unity", _)) = true
   | is_unit _ = false;
 
 
@@ -226,13 +226,13 @@
 
 fun mk_tupleT Ts = foldr mk_prodT (Ts, unitT);
 
-fun dest_tupleT (Type ("unit", [])) = []
+fun dest_tupleT (Type ("Product_Type.unit", [])) = []
   | dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U
   | dest_tupleT T = raise TYPE ("dest_tupleT", [T], []);
 
 fun mk_tuple ts = foldr mk_prod (ts, unit);
 
-fun dest_tuple (Const ("()", _)) = []
+fun dest_tuple (Const ("Product_Type.Unity", _)) = []
   | dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u
   | dest_tuple t = raise TERM ("dest_tuple", [t]);