diff -r 880f31a62784 -r 281d44905cab src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Thu Apr 29 10:51:58 1999 +0200
@@ -124,8 +124,7 @@
 Goal "Cli_prg : \
 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
 \                 Int Invariant giv_meets_ask) \
-\      guarantees (LeadsTo {s. k < size (giv s)}    \
-\                          {s. k < size (rel s)})";
+\      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
 by (rtac Stable_transient_reachable_LeadsTo 1);