--- a/src/HOL/Bali/WellType.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/WellType.thy Tue Mar 14 18:19:10 2023 +0100
@@ -295,7 +295,7 @@
E,dt\<Turnstile>Throw e\<Colon>\<surd>"
\<comment> \<open>cf. 14.18\<close>
| Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
- lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
+ lcl E (VName vn)=None; E \<lparr>lcl := (lcl E)(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
\<Longrightarrow>
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"