--- a/src/HOL/Bali/Eval.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/Eval.thy Fri Jun 15 13:02:12 2018 +0200
@@ -346,7 +346,7 @@
(case k of
EName e
\<Rightarrow> (case e of
- VNam v \<Rightarrow> (empty ((pars m)[\<mapsto>]pvs)) v
+ VNam v \<Rightarrow> (Map.empty ((pars m)[\<mapsto>]pvs)) v
| Res \<Rightarrow> None)
| This
\<Rightarrow> (if mode=Static then None else Some a'))
@@ -362,7 +362,7 @@
EName e
\<Rightarrow> (case e of
VNam v
- \<Rightarrow> (empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
+ \<Rightarrow> (Map.empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
| Res \<Rightarrow> None)
| This
\<Rightarrow> (if mode=Static then None else Some a')))
@@ -578,7 +578,7 @@
if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>
+ G\<turnstile>set_lvars Map.empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>
\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
\<comment> \<open>This class initialisation rule is a little bit inaccurate. Look at the
@@ -1022,7 +1022,7 @@
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0
else G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>
+ G\<turnstile>set_lvars Map.empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
apply (rule eval.Init)