# HG changeset patch # User wenzelm # Date 1001622249 -7200 # Node ID 8e45a16295ed9de6c714423598b0d3d13f0276b5 # Parent 14b03d1463d418a99da5b9dcd494ae5282c1c546 HOLogic.unit; diff -r 14b03d1463d4 -r 8e45a16295ed src/HOL/Hoare/Hoare.ML --- 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;