src/HOL/Bali/WellForm.thy

   qed
 qed
 
 lemma dynmethd_Object:
   assumes statM: "methd G Object sig = Some statM" and
-        private: "accmodi statM = Private" and 
+        "private": "accmodi statM = Private" and 
        is_cls_C: "is_class G C" and
              wf: "wf_prog G"
   shows "dynmethd G Object C sig = Some statM"
 proof -
   from is_cls_C wf 

   from wf have ws: "ws_prog G" 
     by simp
   from wf 
   have is_cls_Obj: "is_class G Object" 
     by simp
-  from statM subclseq is_cls_Obj ws private
+  from statM subclseq is_cls_Obj ws "private"
   show ?thesis
   proof (cases rule: dynmethd_cases)
     case Static then show ?thesis .
   next
     case Overrides 
-    with private show ?thesis 
+    with "private" show ?thesis 
       by (auto dest: no_Private_override)
   qed
 qed
 
 lemma wf_imethds_hiding_objmethdsD: