# HG changeset patch
# User wenzelm
# Date 1127252217 -7200
# Node ID 3825229092f03503d5706f6eeb5766700ca3be87
# Parent  1b7c2f7df2e62c5eb16f50baae6b35ada36312c6
fixed proof script of lemma merges_same_conv (Why did it stop working?);

diff -r 1b7c2f7df2e6 -r 3825229092f0 src/HOL/MicroJava/BV/Kildall.thy
--- 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