--- a/src/HOL/Bali/WellForm.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/WellForm.thy Tue Mar 14 18:19:10 2023 +0100
@@ -85,7 +85,7 @@
EName e
\<Rightarrow> (case e of
VNam v
- \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
+ \<Rightarrow>((table_of (lcls (mbody m)))(pars m [\<mapsto>] parTs sig)) v
| Res \<Rightarrow> Some (resTy m))
| This \<Rightarrow> if is_static m then None else Some (Class C)))"
@@ -110,7 +110,7 @@
lemma callee_lcl_VNam_simp [simp]:
"callee_lcl C sig m (EName (VNam v))
- = (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v"
+ = ((table_of (lcls (mbody m)))(pars m [\<mapsto>] parTs sig)) v"
by (simp add: callee_lcl_def)
lemma callee_lcl_Res_simp [simp]: