src/HOL/UNITY/TimerArray.ML

--- a/src/HOL/UNITY/TimerArray.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -26,6 +26,7 @@
 qed "Timer_preserves_snd";
 AddIffs [Timer_preserves_snd];
 
+Addsimps [PLam_stable];
 
 Goal "finite I \
 \     ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";