diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sat Feb 08 16:05:33 2003 +0100
@@ -18,7 +18,7 @@
     "decr == UN n uu. {((Suc n, uu), (n,uu))}"
   
   Timer :: "'a state program"
-    "Timer == mk_program (UNIV, {decr}, UNIV)"
+    "Timer == mk_total_program (UNIV, {decr}, UNIV)"
 
 
 declare Timer_def [THEN def_prg_Init, simp]
@@ -61,8 +61,8 @@
 apply (rename_tac "n")
 apply (rule PLam_leadsTo_Basis)
 apply (auto simp add: lessThan_Suc [symmetric])
-apply (unfold Timer_def, constrains) 
-apply (rule_tac act = decr in transientI, auto)
+apply (unfold Timer_def mk_total_program_def, constrains) 
+apply (rule_tac act = decr in totalize_transientI, auto)
 done
 
 end