--- a/src/HOL/MicroJava/BV/Kildall.thy Tue Sep 20 22:07:36 2005 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Sep 20 23:36:57 2005 +0200
@@ -127,7 +127,9 @@
apply (rule iffI)
apply (rule context_conjI)
apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
- apply (force dest!: le_listD simp add: nth_list_update)
+ apply (drule_tac p = p in le_listD)
+ apply simp
+ apply simp
apply (erule subst, rule merges_incr)
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
apply clarify