src/HOL/UNITY/Client.thy
changeset 6012 1894bfc4aee9
parent 5804 8e0a4c4fd67b
child 6295 351b3c2b0d83
--- a/src/HOL/UNITY/Client.thy	Wed Dec 02 16:14:09 1998 +0100
+++ b/src/HOL/UNITY/Client.thy	Thu Dec 03 10:45:06 1998 +0100
@@ -48,7 +48,8 @@
 		          size (ask s) = size (rel s))}"
 
   Cli_prg :: state program
-    "Cli_prg == mk_program ({s. tok s : atMost Max &
+    "Cli_prg == mk_program (UNIV,
+			    {s. tok s : atMost Max &
 			        giv s = [] &
 			        ask s = [] &
 			        rel s = []},