# HG changeset patch
# User wenzelm
# Date 1426168712 -3600
# Node ID d662d096f72b40ea386bf0870d5f1932d7d88847
# Parent  55eb8932d539b8b4e28dd5dd3d51022ac37b76d2
quote "method" to allow Eisbach using this keyword;

diff -r 55eb8932d539 -r d662d096f72b src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Thu Mar 12 14:58:32 2015 +0100
@@ -368,7 +368,7 @@
 class) to a qualified member declaration:  @{text method}  *}
 
 definition
-  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+  "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
   where "method sig m = (declclass m, mdecl (sig, mthd m))"
 
 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
diff -r 55eb8932d539 -r d662d096f72b src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 12 14:58:32 2015 +0100
@@ -429,14 +429,14 @@
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
   assumes is_class: "is_class \<Gamma> C"
-    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     and m: "m \<noteq> init"
   defines start: "s \<equiv> start_state \<Gamma> C m"
 
   assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t" 
   shows "t \<noteq> TypeError"
 proof -
-  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
     unfolding start by (rule BV_correct_initial)
   from wt this s show ?thesis by (rule no_type_errors)
 qed
@@ -461,12 +461,12 @@
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
   assumes is_class: "is_class \<Gamma> C"
-    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     and m: "m \<noteq> init"
   defines start: "s \<equiv> start_state \<Gamma> C m"
   shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
 proof -
-  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
     unfolding start by (rule BV_correct_initial)
   with wt show ?thesis by (rule welltyped_commutes)
 qed
diff -r 55eb8932d539 -r d662d096f72b src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 12 14:58:32 2015 +0100
@@ -811,7 +811,7 @@
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
 proof -
   assume wtprog: "wt_jvm_prog G phi"
-  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+  assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   assume ins:    "ins ! pc = Invoke C' mn pTs"
   assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
   assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
@@ -823,7 +823,7 @@
     wfprog: "wf_prog wfmb G" 
     by (simp add: wt_jvm_prog_def)
       
-  from ins method approx
+  from ins "method" approx
   obtain s where
     heap_ok: "G\<turnstile>h hp\<surd>" and
     prealloc:"preallocated hp" and
@@ -880,7 +880,7 @@
   from stk' l_o l
   have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
 
-  with state' method ins no_xcp oX_conf
+  with state' "method" ins no_xcp oX_conf
   obtain ref where oX_Addr: "oX = Addr ref"
     by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
 
@@ -922,7 +922,7 @@
       
   from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
 
-  with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
+  with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
   have state'_val:
     "state' =
      Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
@@ -972,7 +972,7 @@
     show ?thesis by (simp add: correct_frame_def)
   qed
 
-  from state'_val heap_ok mD'' ins method phi_pc s X' l mX
+  from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
        frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
   show ?thesis
     apply (simp add: correct_state_def)
diff -r 55eb8932d539 -r d662d096f72b src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Mar 12 14:58:32 2015 +0100
@@ -177,7 +177,7 @@
 qed
 
 consts
-  method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
+  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
   field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
   fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
 
diff -r 55eb8932d539 -r d662d096f72b src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Thu Mar 12 14:58:32 2015 +0100
@@ -108,7 +108,7 @@
 done
 
 --{* Methods of a class, with inheritance and hiding *}
-definition method :: "cname => (mname \<rightharpoonup> methd)" where
+definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
   "method C \<equiv> class_rec C methods"
 
 lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>