diff -r bbd2f7b00736 -r a34d89ce6097 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon May 26 18:36:15 2003 +0200
@@ -239,11 +239,11 @@
   done
 
 lemma order_sup_state_opt:
-  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
+  "ws_prog G \<Longrightarrow> order (sup_state_opt G)"
   by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
 
 theorem exec_mono:
-  "wf_prog wf_mb G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
+  "ws_prog G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
   mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
   apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
   apply (rule mono_lift)
@@ -257,7 +257,7 @@
   done
 
 theorem semilat_JVM_slI:
-  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
+  "ws_prog G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
   apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
   apply (rule semilat_opt)
   apply (rule err_semilat_Product_esl)
@@ -287,7 +287,7 @@
          "(C,S,fs,mdecls) \<in> set G"
          "((mn,pTs),rT,code) \<in> set mdecls"
   hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
-    by (unfold wf_prog_def wf_cdecl_def) auto  
+    by (rule wf_prog_wf_mdecl)
   hence "\<forall>t \<in> set pTs. is_type G t" 
     by (unfold wf_mdecl_def wf_mhead_def) auto
   moreover
@@ -319,11 +319,10 @@
     apply (unfold wf_prog_def wf_cdecl_def)
     apply clarsimp
     apply (drule bspec, assumption)
-    apply (unfold wf_mdecl_def)
+    apply (unfold wf_cdecl_mdecl_def)
     apply clarsimp
     apply (drule bspec, assumption)
-    apply clarsimp
-    apply (frule methd [OF wf], 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+)