diff -r bfba0eb5124b -r b06cc3834ee5 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Fri Nov 16 22:11:19 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Fri Nov 16 23:02:58 2001 +0100
@@ -47,15 +47,13 @@
  apply clarify
  apply (case_tac "bs!p")
 
+ apply (fastsimp simp add: not_Err_eq dest: subsetD nth_mem)
  apply fastsimp
+ apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
  apply fastsimp
+ apply (fastsimp dest: field_fields fields_is_type)
  apply fastsimp
  apply fastsimp
- apply clarsimp
- defer
- apply fastsimp
- apply fastsimp
- apply clarsimp
  defer
  apply fastsimp
  apply fastsimp
@@ -66,21 +64,11 @@
  apply fastsimp
  apply fastsimp
  apply fastsimp
- defer
 
  (* Invoke *)
- apply (simp add: Un_subset_iff)
+ apply (clarsimp simp add: Un_subset_iff)
  apply (drule method_wf_mdecl, assumption+)
  apply (simp add: wf_mdecl_def wf_mhead_def)
-
- (* Getfield *)
- 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