diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Thu Jun 02 13:47:08 2005 +0200
@@ -35,7 +35,7 @@
 
 lemma Timer_preserves_snd [iff]: "Timer : preserves snd"
 apply (rule preservesI)
-apply (unfold Timer_def, constrains)
+apply (unfold Timer_def, safety)
 done
 
 
@@ -49,7 +49,7 @@
 apply auto
 (*Safety property, already reduced to the single Timer case*)
  prefer 2
- apply (simp add: Timer_def, constrains) 
+ apply (simp add: Timer_def, safety) 
 (*Progress property for the array of Timers*)
 apply (rule_tac f = "sub i o fst" in lessThan_induct)
 apply (case_tac "m")
@@ -61,7 +61,7 @@
 apply (rename_tac "n")
 apply (rule PLam_leadsTo_Basis)
 apply (auto simp add: lessThan_Suc [symmetric])
-apply (unfold Timer_def mk_total_program_def, constrains) 
+apply (unfold Timer_def mk_total_program_def, safety) 
 apply (rule_tac act = decr in totalize_transientI, auto)
 done