# HG changeset patch
# User wenzelm
# Date 1316778224 -7200
# Node ID 73accf69135d340a7c27673c8307728fced3fb76
# Parent  54c832311598b6da4087c1532a26e2a08c5f78ba
tuned proof;

diff -r 54c832311598 -r 73accf69135d src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Sep 23 10:31:12 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Sep 23 13:43:44 2011 +0200
@@ -1270,7 +1270,7 @@
 lemma correct_state_impl_Some_method:
   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
   \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
-by (auto simp add: correct_state_def Let_def)
+by (auto simp add: correct_state_def)
 
 
 lemma BV_correct_1 [rule_format]: