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;