diff -r 5f10ca5e0b49 -r 01181fdbc9f0 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Mon Mar 26 16:31:38 2001 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy	Mon Mar 26 19:37:31 2001 +0200
@@ -139,7 +139,6 @@
   "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
 apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
 apply (simp split: err.split)
-apply blast
 done
 
 lemma err_semilat_eslI: