HOLogic.unit;

--- a/src/HOL/Hoare/Hoare.ML	Thu Sep 27 22:23:40 2001 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Thu Sep 27 22:24:09 2001 +0200
@@ -87,7 +87,7 @@
           $ absfree (n, T, z) end end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
-fun mk_bodyC []      = Const ("()", unitT) 
+fun mk_bodyC []      = HOLogic.unit
   | mk_bodyC (x::xs) = if xs=[] then x 
                else let val (n, T) = dest_Free x ;
                         val z = mk_bodyC xs;