diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/WellForm.thy
--- 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]: