diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Handshake.thy
--- a/src/HOL/UNITY/Comp/Handshake.thy	Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Handshake.thy	Sat Feb 08 16:05:33 2003 +0100
@@ -21,14 +21,14 @@
     "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
 
   F :: "state program"
-    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
+    "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
 
   (*G's program*)
   cmdG :: "(state*state) set"
     "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
 
   G :: "state program"
-    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
+    "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
 
   (*the joint invariant*)
   invFG :: "state set"