--- a/src/HOL/MicroJava/BV/JVM.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Tue Feb 26 15:45:32 2002 +0100
@@ -107,14 +107,14 @@
apply clarsimp
apply (erule disjE)
apply (fastsimp dest: field_fields fields_is_type)
- apply simp
+ apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
apply clarsimp
apply (erule disjE)
apply fastsimp
- apply simp
+ apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp