# HG changeset patch
# User nipkow
# Date 1063638900 -7200
# Node ID 2014eac694d27cd21611e17ff91797bc783d73e4
# Parent  609c072edf9028617df77f3bddd24fc921b4bf59
Mod due to new thm in Map.

diff -r 609c072edf90 -r 2014eac694d2 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 15 14:00:43 2003 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 15 17:15:00 2003 +0200
@@ -198,7 +198,6 @@
   apply clarify  
   apply simp
   apply (rule conjI) 
-   apply (simp add: nth_list_update)
    apply blast
   apply (simp add: nth_list_update)
   apply blast
@@ -471,4 +470,4 @@
 apply (blast intro!: le_listD less_lengthI)
 done
 
-end
\ No newline at end of file
+end