diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -815,7 +815,7 @@
   wf_mhead G P sig mh;
   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   G,s\<turnstile>Map.empty (pars mh[\<mapsto>]pvs)
-      [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
+      [\<sim>\<Colon>\<preceq>](table_of lvars)(pars mh[\<mapsto>]parTs sig)"
 apply (unfold wf_mhead_def)
 apply clarify
 apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
@@ -895,7 +895,7 @@
                 (case k of
                    EName e \<Rightarrow> (case e of 
                                  VNam v 
-                                  \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
+                                  \<Rightarrow> ((table_of (lcls (mbody (mthd dm))))
                                         (pars (mthd dm)[\<mapsto>]parTs sig)) v
                                | Res \<Rightarrow> Some (resTy (mthd dm)))
                  | This \<Rightarrow> if (is_static (mthd sm)) 
@@ -1180,7 +1180,7 @@
 
 lemma map_upds_upd_eq_length_simp:
   "\<And> tab qs x y. length ps = length qs 
-                  \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
+                  \<Longrightarrow> tab(ps[\<mapsto>]qs, x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
 proof (induct "ps")
   case Nil thus ?case by simp
 next
@@ -1189,7 +1189,7 @@
   obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length 
-  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
+  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs', x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
     by (rule Cons.hyps)
   with qs show ?case
     by simp
@@ -1219,7 +1219,7 @@
     show ?thesis by simp
   next
     case (Cons y ys')
-    have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
+    have "(tab(x\<mapsto>y, xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y, xs[\<mapsto>]ys')) z"
       by (iprover intro: Hyps map_upd_cong_ext)
     with Cons show ?thesis
       by simp
@@ -1230,7 +1230,7 @@
   by simp
 
 lemma map_upds_eq_length_suffix: "\<And> tab qs. 
-        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
+        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs, xs[\<mapsto>][])"
 proof (induct ps)
   case Nil thus ?case by simp
 next
@@ -1238,7 +1238,7 @@
   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length
-  have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
+  have "tab(p\<mapsto>q, ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q, ps[\<mapsto>]qs', xs[\<mapsto>][])"
     by (rule Cons.hyps)
   with qs show ?case 
     by simp
@@ -1247,7 +1247,7 @@
   
 lemma map_upds_upds_eq_length_prefix_simp:
   "\<And> tab qs. length ps = length qs
-              \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
+              \<Longrightarrow> tab(ps[\<mapsto>]qs, xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
 proof (induct ps)
   case Nil thus ?case by simp
 next
@@ -1255,7 +1255,7 @@
   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length 
-  have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
+  have "tab(p\<mapsto>q, ps[\<mapsto>]qs', xs[\<mapsto>]ys) = tab(p\<mapsto>q, ps @ xs[\<mapsto>](qs' @ ys))"
     by (rule Cons.hyps)
   with qs 
   show ?case by simp
@@ -1297,11 +1297,11 @@
 
 
 lemma map_upd_Some_swap:
- "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
+ "(tab(r\<mapsto>w, u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v, r\<mapsto>w)) vn = Some z"
 by (simp add: fun_upd_def)
 
 lemma map_upd_None_swap:
- "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
+ "(tab(r\<mapsto>w, u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v, r\<mapsto>w)) vn = None"
 by (simp add: fun_upd_def)
 
 
@@ -1331,7 +1331,7 @@
     show ?thesis
     proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
       case True
-      with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
+      with some ys have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = Some z"
         by (fastforce intro: Cons.hyps)
       with ys show ?thesis 
         by simp
@@ -1345,7 +1345,7 @@
       ultimately
       have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
         by simp
-      hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
+      hence "(tab(x\<mapsto>y, xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn"
         by (rule map_upds_cong_ext)
       with some ys
       show ?thesis 
@@ -1355,18 +1355,18 @@
 qed
    
 lemma map_upds_Some_swap: 
- assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
-    shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
-proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
+ assumes r_u: "(tab(r\<mapsto>w, u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
+    shows "\<exists> z. (tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
+proof (cases "(tab(r\<mapsto>w, u\<mapsto>v)) vn = Some z")
   case True
-  then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
+  then obtain z' where "(tab(u\<mapsto>v, r\<mapsto>w)) vn = Some z'"
     by (rule map_upd_Some_swap [elim_format]) blast
-  thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
+  thus "\<exists> z. (tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
     by (rule map_upds_Some_expand)
 next
   case False
   with r_u
-  have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
+  have "(tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
     by (rule map_upds_in_expansion_map_swap)
   thus ?thesis
     by simp
@@ -1374,7 +1374,7 @@
  
 lemma map_upds_Some_insert:
   assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
-    shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
+    shows "\<exists> z. (tab(u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
 proof (cases "\<exists> z. tab vn = Some z")
   case True
   then obtain z' where "tab vn = Some z'" by blast
@@ -1386,7 +1386,7 @@
   case False
   hence "tab vn \<noteq> Some z" by simp
   with z
-  have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
+  have "(tab(u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
     by (rule map_upds_in_expansion_map_swap)
   thus ?thesis ..
 qed
@@ -1425,7 +1425,7 @@
     have "(tab(x\<mapsto>y)) vn = Some el"
       by - (rule Cons.hyps,auto)
     moreover from tab'_vn ys
-    have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
+    have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = None" 
       by simp
     hence "(tab'(x\<mapsto>y)) vn = None"
       by (rule map_upds_None_cut)
@@ -1436,7 +1436,7 @@
 
    
 lemma dom_vname_split:
- "dom (case_lname (case_ename (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
+ "dom (case_lname (case_ename (tab(x\<mapsto>y, xs[\<mapsto>]ys)) a) b)
    = dom (case_lname (case_ename (tab(x\<mapsto>y)) a) b) \<union> 
      dom (case_lname (case_ename (tab(xs[\<mapsto>]ys)) a) b)"
   (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
@@ -1503,7 +1503,7 @@
     case Nil with len show ?thesis by simp
   next
     case (Cons y tl)
-    with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
+    with len have "dom (tab(x\<mapsto>y, xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
       by - (rule Hyp,simp)
     moreover 
     have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
@@ -3162,7 +3162,7 @@
                     EName e
                     \<Rightarrow> (case e of 
                           VNam v 
-                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
+                          \<Rightarrow>((table_of (lcls (mbody (mthd dynM))))
                              (pars (mthd dynM)[\<mapsto>]pTs')) v
                         | Res \<Rightarrow> Some (resTy dynM))
                   | This \<Rightarrow> if is_static statM