--- a/src/HOLCF/ex/Hoare.ML Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/ex/Hoare.ML Wed Jun 29 12:03:41 1994 +0200
@@ -90,7 +90,7 @@
]);
val hoare_lemma28 = prove_goal HOLCF.thy
-"b1[y::'a]=UU::tr ==> b1[UU] = UU"
+"b1[y::'a]=(UU::tr) ==> b1[UU] = UU"
(fn prems =>
[
(cut_facts_tac prems 1),