--- 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;
--- 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 *}