src/HOL/Bali/TypeSafe.thy

         case True
         with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
           by simp
         from da_e1 s0_s1 True obtain E1' where
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
-          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
+          by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
         with conf_s1 wt_e1
         obtain 
           "s2\<Colon>\<preceq>(G, L)"
           "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
           "error_free s2"            

         case False
         with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
           by simp
         from da_e2 s0_s1 False obtain E2' where
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
-          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
+          by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
         with conf_s1 wt_e2
         obtain 
           "s2\<Colon>\<preceq>(G, L)"
           "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
           "error_free s2"