src/HOL/UNITY/Reach.thy

--- a/src/HOL/UNITY/Reach.thy	Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy	Thu Oct 01 18:28:18 1998 +0200
@@ -24,8 +24,7 @@
     "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
 
   Rprg :: state program
-    "Rprg == (|Init = {%v. v=init},
-	       Acts0 = (UN (u,v): edges. {asgt u v})|)"
+    "Rprg == mk_program ({%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}"