# HG changeset patch
# User wenzelm
# Date 1001622268 -7200
# Node ID 43abedd4467ead6ac6913ed5615a80089648594e
# Parent  8e45a16295ed9de6c714423598b0d3d13f0276b5
renamed "()" to Unity;

diff -r 8e45a16295ed -r 43abedd4467e src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Thu Sep 27 22:24:09 2001 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Thu Sep 27 22:24:28 2001 +0200
@@ -74,7 +74,7 @@
                               absfree ((fst o dest_Free) v, dummyT, mk_abstuple w body);
 
   
-fun mk_fbody v e []      = Syntax.const "()"
+fun mk_fbody v e []      = Syntax.const "Unity"
   | mk_fbody v e [x]     = if v=x then e else x
   | mk_fbody v e (x::xs) = Syntax.const "Pair" $ (if v=x then e else x) $
                            mk_fbody v e xs;
diff -r 8e45a16295ed -r 43abedd4467e src/HOL/ex/Tuple.thy
--- a/src/HOL/ex/Tuple.thy	Thu Sep 27 22:24:09 2001 +0200
+++ b/src/HOL/ex/Tuple.thy	Thu Sep 27 22:24:28 2001 +0200
@@ -24,7 +24,7 @@
   fst :: "('a, 'b) prod => 'a"
   snd :: "('a, 'b) prod => 'b"
   split :: "('a => 'b => 'c) => ('a, 'b) prod => 'c"
-  "()" :: unit  ("'(')")
+  Unity :: unit    ("'(')")
 
 
 subsection {* Concrete syntax *}