diff -r 70d5f2f7d27f -r 0b30bde83185 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Jul 12 15:37:48 2013 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Jul 12 15:39:46 2013 +0200
@@ -301,21 +301,19 @@
  
   shows 
   "wf_prog (\<lambda>G C bd. Q G C bd) G"
-proof -
-  from wf show ?thesis
-    apply (unfold wf_prog_def wf_cdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (unfold wf_cdecl_mdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
-    apply (frule is_type_pTs [OF wf], assumption+)
-    apply clarify
-    apply (drule rule [OF wf], assumption+)
-    apply (rule HOL.refl)
-    apply assumption+
-    done
-qed
+  using wf
+  apply (unfold wf_prog_def wf_cdecl_def)
+  apply clarsimp
+  apply (drule bspec, assumption)
+  apply (unfold wf_cdecl_mdecl_def)
+  apply clarsimp
+  apply (drule bspec, assumption)
+  apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
+  apply (frule is_type_pTs [OF wf], assumption+)
+  apply clarify
+  apply (drule rule [OF wf], assumption+)
+  apply (rule HOL.refl)
+  apply assumption+
+  done
 
 end