diff -r 886655a150f6 -r d1b97708d5eb src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -346,7 +346,7 @@
   with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" by (rule wtc_mono)
   with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp
   moreover
-  assume s: "s \<noteq> \<top>" 
+  assume s': "s \<noteq> \<top>" 
   ultimately
   have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp
   moreover {
@@ -357,23 +357,23 @@
     moreover
     from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" 
       by (auto simp add: cert_ok_def)
-    with pres have "wtc c pc s \<in> A" by (rule wtc_pres)
+    from pres this s pc have "wtc c pc s \<in> A" by (rule wtc_pres)
     ultimately
     have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast
-    with s wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp 
+    with s' wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp
   }
   ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+
 qed
 
   
 theorem (in lbvc) wtl_complete:
-  assumes "wt_step r \<top> step \<phi>"
-  assumes "s <=_r \<phi>!0" and "s \<in> A" and "s \<noteq> \<top>" and "length ins = length phi"
+  assumes wt: "wt_step r \<top> step \<phi>"
+    and s: "s <=_r \<phi>!0" "s \<in> A" "s \<noteq> \<top>"
+    and len: "length ins = length phi"
   shows "wtl ins c 0 s \<noteq> \<top>"
-proof -  
-  have "0+length ins = length phi" by simp
-  thus ?thesis by - (rule wt_step_wtl_lemma)
+proof -
+  from len have "0+length ins = length phi" by simp
+  from wt this s show ?thesis by (rule wt_step_wtl_lemma)
 qed
 
-
 end