src/HOL/Hoare/Hoare.thy

   | mk_abstuple [v]    body = absfree ((fst o dest_Free) v, dummyT, body)
   | mk_abstuple (v::w) body = Syntax.const "split" $
                               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;
 
 fun mk_fexp v e xs = mk_abstuple xs (mk_fbody v e xs);