1.1 --- a/src/HOL/Bali/WellForm.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -2788,7 +2788,7 @@
     1.4        proof -
     1.5          from im statM statT isT_statT wf not_Private_statM 
     1.6          have "is_static im = is_static statM"
     1.7 -          by (fastsimp dest: wf_imethds_hiding_objmethdsD)
     1.8 +          by (fastforce dest: wf_imethds_hiding_objmethdsD)
     1.9          with wf isT_statT statT im 
    1.10          have "\<not> is_static statM"
    1.11            by (auto dest: wf_prog_idecl imethds_wf_mhead)