# HG changeset patch
# User wenzelm
# Date 1427905092 -7200
# Node ID d1e7f56bcd793eac1564344c678c0b0c68c4a512
# Parent  e563b0ee0331d9645e9a77119b35fa164638221b
evade popular keyword;

diff -r e563b0ee0331 -r d1e7f56bcd79 src/FOL/ex/Locale_Test/Locale_Test1.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
 
diff -r e563b0ee0331 -r d1e7f56bcd79 src/HOL/Bali/WellForm.thy
--- 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