diff -r d6134fb5a49f -r da3e88ea6c72 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Sat Nov 21 17:35:55 2009 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Nov 21 17:37:07 2009 +0100
@@ -284,8 +284,7 @@
 apply (frule fields_rec, assumption)
 apply (rule HOL.trans)
 apply (simp add: o_def)
-apply (simp (no_asm_use) 
-  add: split_beta split_def o_def map_compose [THEN sym] del: map_compose)
+apply (simp (no_asm_use) add: split_beta split_def o_def)
 done
 
 lemma method_Object [simp]: