updated for is_class changes

--- a/src/HOL/MicroJava/BV/JType.thy	Thu Dec 07 17:59:24 2000 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Thu Dec 07 18:22:17 2000 +0100
@@ -44,7 +44,7 @@
 
 lemma is_tyI:
   "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
-  by (auto simp add: is_ty_def dest: subcls_C_Object 
+  by (auto simp add: is_ty_def intro: subcls_C_Object 
            split: ty.splits ref_ty.splits)
 
 lemma is_type_conv: 

--- a/src/HOL/MicroJava/BV/JVM.thy	Thu Dec 07 17:59:24 2000 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Dec 07 18:22:17 2000 +0100
@@ -143,6 +143,8 @@
   "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
   by blast
 
+lemmas [iff del] = not_None_eq
+
 theorem exec_pres_type:
   "[| wf_prog wf_mb S |] ==> 
       pres_type (exec S maxs rT bs) (size bs) (states S maxs maxr)"
@@ -176,18 +178,22 @@
  defer
 
  apply (simp add: Un_subset_iff)
- apply (drule method_wf_mdecl, assumption)
+ apply (drule method_wf_mdecl, assumption+)
  apply (simp add: wf_mdecl_def wf_mhead_def)
 
- apply (drule fields_is_type)
- apply assumption
- apply (subgoal_tac "((vname, cname), vT) \<in> set (fields (S, cname))")
- apply assumption
-  apply (simp add: field_def)
-  apply (drule map_of_SomeD)
-  apply auto
+ apply (rule_tac fn = "(vname,cname)" in fields_is_type)
+ defer
+ apply assumption+
+ apply (simp add: field_def)
+ apply (drule map_of_SomeD)
+ apply (rule map_of_SomeI)
+ apply (auto simp add: unique_fields)
  done
 
+
+lemmas [iff] = not_None_eq
+
+
 theorem exec_mono:
   "wf_prog wf_mb G ==>
   mono (JVM.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)"