src/HOL/UNITY/Reach.thy

--- a/src/HOL/UNITY/Reach.thy	Wed Dec 02 16:14:09 1998 +0100
+++ b/src/HOL/UNITY/Reach.thy	Thu Dec 03 10:45:06 1998 +0100
@@ -24,7 +24,7 @@
     "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
 
   Rprg :: state program
-    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})"
+    "Rprg == mk_program (UNIV, {%v. v=init}, UN (u,v): edges. {asgt u v})"
 
   reach_invariant :: state set
     "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"