diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Wed Mar 12 22:57:50 2014 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Mar 13 07:07:07 2014 +0100 @@ -565,7 +565,7 @@ apply clarify apply (frule wf_prog_ws_prog) apply (frule fields_Object, assumption+) -apply (simp only: is_class_Object) apply simp +apply (simp only: is_class_Object) apply clarify apply (frule fields_rec)