evade popular keyword;
authorwenzelm
Wed, 01 Apr 2015 18:18:12 +0200
changeset 59897 d1e7f56bcd79
parent 59896 e563b0ee0331
child 59898 81c70bdbd908
evade popular keyword;
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/HOL/Bali/WellForm.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Apr 01 18:17:44 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Apr 01 18:18:12 2015 +0200
@@ -775,7 +775,7 @@
 
 locale container
 begin
-interpretation private!: roundup True by unfold_locales rule
+interpretation "private"!: roundup True by unfold_locales rule
 lemmas true_copy = private.true
 end
 
--- a/src/HOL/Bali/WellForm.thy	Wed Apr 01 18:17:44 2015 +0200
+++ b/src/HOL/Bali/WellForm.thy	Wed Apr 01 18:18:12 2015 +0200
@@ -1979,7 +1979,7 @@
 
 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"
@@ -1992,13 +1992,13 @@
   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