diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Client.thy	Sat Feb 08 16:05:33 2003 +0100
@@ -30,10 +30,10 @@
   
   rel_act :: "('a state_d * 'a state_d) set"
     "rel_act == {(s,s').
-		  EX nrel. nrel = size (rel s) &
-		           s' = s (| rel := rel s @ [giv s!nrel] |) &
-		           nrel < size (giv s) &
-		           ask s!nrel <= giv s!nrel}"
+		  \\<exists>nrel. nrel = size (rel s) &
+		         s' = s (| rel := rel s @ [giv s!nrel] |) &
+		         nrel < size (giv s) &
+		         ask s!nrel <= giv s!nrel}"
 
   (** Choose a new token requirement **)
 
@@ -49,10 +49,11 @@
 
   Client :: 'a state_d program
     "Client ==
-       mk_program ({s. tok s : atMost NbT &
-		    giv s = [] & ask s = [] & rel s = []},
-		   {rel_act, tok_act, ask_act},
-		   UN G: preserves rel Int preserves ask Int preserves tok.
+       mk_total_program
+            ({s. tok s : atMost NbT &
+		 giv s = [] & ask s = [] & rel s = []},
+	     {rel_act, tok_act, ask_act},
+	     \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
 		   Acts G)"
 
   (*Maybe want a special theory section to declare such maps*)