fixed proof script of lemma merges_same_conv (Why did it stop working?);

--- 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