1.1 --- a/src/HOL/Bali/WellForm.thy	Wed Apr 01 18:17:44 2015 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Wed Apr 01 18:18:12 2015 +0200
     1.3 @@ -1979,7 +1979,7 @@
     1.4  
     1.5  lemma dynmethd_Object:
     1.6    assumes statM: "methd G Object sig = Some statM" and
     1.7 -        private: "accmodi statM = Private" and 
     1.8 +        "private": "accmodi statM = Private" and 
     1.9         is_cls_C: "is_class G C" and
    1.10               wf: "wf_prog G"
    1.11    shows "dynmethd G Object C sig = Some statM"
    1.12 @@ -1992,13 +1992,13 @@
    1.13    from wf 
    1.14    have is_cls_Obj: "is_class G Object" 
    1.15      by simp
    1.16 -  from statM subclseq is_cls_Obj ws private
    1.17 +  from statM subclseq is_cls_Obj ws "private"
    1.18    show ?thesis
    1.19    proof (cases rule: dynmethd_cases)
    1.20      case Static then show ?thesis .
    1.21    next
    1.22      case Overrides 
    1.23 -    with private show ?thesis 
    1.24 +    with "private" show ?thesis 
    1.25        by (auto dest: no_Private_override)
    1.26    qed
    1.27  qed