diff --git a/lib/BCorres_UL.thy b/lib/BCorres_UL.thy
index 6d4cf930b..86d108b51 100644
--- a/lib/BCorres_UL.thy
+++ b/lib/BCorres_UL.thy
@@ -17,12 +17,12 @@ definition bcorres_underlying where
   "bcorres_underlying t f g \<equiv> \<forall>s. s_bcorres_underlying t f g s"
 
 lemma wpc_helper_bcorres:
-  "bcorres_underlying t f g \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (bcorres_underlying t f g)"
-  by (simp add: wpc_helper_def)
+  "bcorres_underlying t f g \<Longrightarrow>  wpc_helper P Q (bcorres_underlying t f g)"
+  by (simp add: wpc_helper_def split: prod.split)
 
 lemma wpc_helper_s_bcorres:
-  "s_bcorres_underlying t f g s \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (s_bcorres_underlying t f g s)"
-  by (simp add: wpc_helper_def)
+  "s_bcorres_underlying t f g s \<Longrightarrow>  wpc_helper P Q (s_bcorres_underlying t f g s)"
+  by (simp add: wpc_helper_def split: prod.split)
 
 wpc_setup "\<lambda>f. bcorres_underlying t f g" wpc_helper_bcorres
 wpc_setup "\<lambda>f. s_bcorres_underlying t f g s" wpc_helper_bcorres
diff --git a/lib/Bisim_UL.thy b/lib/Bisim_UL.thy
index bc4b981ee..9c75e9ef9 100644
--- a/lib/Bisim_UL.thy
+++ b/lib/Bisim_UL.thy
@@ -159,7 +159,7 @@ lemma bisim_split_handle:
 
 (* Set up wpc *)
 lemma wpc_helper_bisim:
-  "bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (bisim_underlying SR r P (\<lambda>s. s \<in> P') f f')"
+  "bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (bisim_underlying SR r P P' f f')"
   apply (clarsimp simp: wpc_helper_def)
   apply (erule bisim_guard_imp)
    apply simp
@@ -342,7 +342,7 @@ lemmas dets_to_det_on [wp] = det_det_on [OF det_gets] det_det_on [OF return_det]
 
 (* Set up wpc *)
 lemma wpc_helper_det_on:
-  "det_on Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (det_on P f)"
+  "det_on Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (det_on P f)"
   apply (clarsimp simp: wpc_helper_def det_on_def)
   done
 
@@ -426,7 +426,7 @@ lemma not_empty_gets [wp]:
 
 (* Set up wpc *)
 lemma wpc_helper_not_empty:
-  "not_empty Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (not_empty P f)"
+  "not_empty Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (not_empty P f)"
   apply (clarsimp simp: wpc_helper_def not_empty_def)
   done
 
diff --git a/lib/EquivValid.thy b/lib/EquivValid.thy
index 9db706502..3ab513ee3 100644
--- a/lib/EquivValid.thy
+++ b/lib/EquivValid.thy
@@ -572,10 +572,10 @@ lemmas pre_ev =
   hoare_pre
   equiv_valid_guard_imp
 
-subsection\<open>Tom instantiates wpc\<close>
+subsection\<open>wpc setup\<close>
 
 lemma wpc_helper_equiv_valid:
-  "equiv_valid D A B Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (equiv_valid D A B P f)"
+  "equiv_valid D A B Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (equiv_valid D A B P f)"
   using equiv_valid_guard_imp
   apply (simp add: wpc_helper_def)
   apply (blast)
diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy
index 0b869889a..22c20ea2c 100644
--- a/lib/MonadicRewrite.thy
+++ b/lib/MonadicRewrite.thy
@@ -710,12 +710,13 @@ lemmas corres_gets_the_bind
 text \<open>Tool integration\<close>
 
 lemma wpc_helper_monadic_rewrite:
-  "monadic_rewrite F E Q' m m'
-   \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (monadic_rewrite F E (\<lambda>s. s \<in> P') m m')"
+  "monadic_rewrite F E Q m m'
+   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (monadic_rewrite F E P m m')"
   by (auto simp: wpc_helper_def elim!: monadic_rewrite_guard_imp)
 
 wpc_setup "\<lambda>m. monadic_rewrite F E Q' m m'" wpc_helper_monadic_rewrite
 wpc_setup "\<lambda>m. monadic_rewrite F E Q' (m >>= c) m'" wpc_helper_monadic_rewrite
+wpc_setup "\<lambda>m. monadic_rewrite F E Q' (m >>=E c) m'" wpc_helper_monadic_rewrite
 
 text \<open>Tactics\<close>
 
diff --git a/lib/Monads/Empty_Fail.thy b/lib/Monads/Empty_Fail.thy
index 7b75a3680..e1418d81b 100644
--- a/lib/Monads/Empty_Fail.thy
+++ b/lib/Monads/Empty_Fail.thy
@@ -27,7 +27,7 @@ definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" wh
 subsection \<open>WPC setup\<close>
 
 lemma wpc_helper_empty_fail_final:
-  "empty_fail f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (empty_fail f)"
+  "empty_fail f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (empty_fail f)"
   by (clarsimp simp: wpc_helper_def)
 
 wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail_final
diff --git a/lib/Monads/No_Fail.thy b/lib/Monads/No_Fail.thy
index 9736a0874..f273069f3 100644
--- a/lib/Monads/No_Fail.thy
+++ b/lib/Monads/No_Fail.thy
@@ -32,7 +32,7 @@ lemma no_fail_pre[wp_pre]:
   by (simp add: no_fail_def)
 
 lemma wpc_helper_no_fail_final:
-  "no_fail Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (no_fail P f)"
+  "no_fail Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_fail P f)"
   by (clarsimp simp: wpc_helper_def elim!: no_fail_pre)
 
 wpc_setup "\<lambda>m. no_fail P m" wpc_helper_no_fail_final
diff --git a/lib/Monads/NonDetMonadVCG.thy b/lib/Monads/NonDetMonadVCG.thy
index d897db607..2cc8f4ed4 100644
--- a/lib/Monads/NonDetMonadVCG.thy
+++ b/lib/Monads/NonDetMonadVCG.thy
@@ -120,19 +120,19 @@ lemmas hoare_pre [wp_pre] =
 subsection \<open>Setting up the precondition case splitter.\<close>
 
 lemma wpc_helper_valid:
-  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>"
+  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_validE:
-  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_validE_R:
-  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
+  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_validR_R:
-  "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>"
+  "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 
diff --git a/lib/Monads/NonDetMonad_Total.thy b/lib/Monads/NonDetMonad_Total.thy
index 7ad256f5a..b4f2f5d66 100644
--- a/lib/Monads/NonDetMonad_Total.thy
+++ b/lib/Monads/NonDetMonad_Total.thy
@@ -40,7 +40,7 @@ lemma validE_NF_alt_def:
 subsection \<open>@{method wpc} setup\<close>
 
 lemma wpc_helper_validNF:
-  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
+  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
   unfolding wpc_helper_def
   by clarsimp (metis hoare_vcg_precond_imp no_fail_pre validNF_def)
 
diff --git a/lib/Monads/TraceMonadVCG.thy b/lib/Monads/TraceMonadVCG.thy
index e88d79b9b..0d13ad337 100644
--- a/lib/Monads/TraceMonadVCG.thy
+++ b/lib/Monads/TraceMonadVCG.thy
@@ -1965,32 +1965,33 @@ lemma hoare_K_bind [wp]:
 text \<open>Setting up the precondition case splitter.\<close>
 
 lemma wpc_helper_valid:
-  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>"
+  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_validE:
-  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_validE_R:
-  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
+  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_validR_R:
-  "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>"
+  "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>"
   by (clarsimp simp: wpc_helper_def elim!: hoare_pre)
 
 lemma wpc_helper_no_fail_final:
-  "no_fail Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (no_fail P f)"
+  "no_fail Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_fail P f)"
   by (clarsimp simp: wpc_helper_def elim!: no_fail_pre)
 
 lemma wpc_helper_validNF:
-  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
+  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
   apply (clarsimp simp: wpc_helper_def)
   by (metis hoare_wp_combs(2) no_fail_pre validNF_def)
 
+(* FIXME: this needs adjustment, case_prod Q is unlikely to unify *)
 lemma wpc_helper_validI:
-  "(\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>) \<Longrightarrow> wpc_helper (P, P') (case_prod Q, Q') (\<lbrace>curry P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>)"
+  "(\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>) \<Longrightarrow> wpc_helper (P, P', P'') (case_prod Q, Q', Q'') (\<lbrace>curry P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>)"
   by (clarsimp simp: wpc_helper_def elim!: validI_weaken_pre)
 
 wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>" wpc_helper_valid
diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy
index a1555b597..6bc3ac1bc 100644
--- a/proof/access-control/CNode_AC.thy
+++ b/proof/access-control/CNode_AC.thy
@@ -727,7 +727,7 @@ lemmas[monad_commute_wp] =
 
 (* Sort-of VCG for monad_commute goals *)
 lemma wpc_helper_monad_commute:
-  "monad_commute P f g \<Longrightarrow> wpc_helper (P, P') (Q, Q') (monad_commute P f g)"
+  "monad_commute P f g \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (monad_commute P f g)"
   by (clarsimp simp: wpc_helper_def)
 
 wpc_setup "\<lambda>m. monad_commute P f m" wpc_helper_monad_commute
diff --git a/proof/crefine/lib/AutoCorres_C.thy b/proof/crefine/lib/AutoCorres_C.thy
index e32ea07f8..2656ef7ee 100644
--- a/proof/crefine/lib/AutoCorres_C.thy
+++ b/proof/crefine/lib/AutoCorres_C.thy
@@ -807,7 +807,7 @@ context kernel begin
 
 lemma wpc_helper_corres_final:
   "corres_underlying sr nf nf' rv Q Q' f f'
-   \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (corres_underlying sr nf nf' rv P (\<lambda>s. s \<in> P') f f')"
+   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (corres_underlying sr nf nf' rv P P' f f')"
   apply (clarsimp simp: wpc_helper_def)
   apply (erule corres_guard_imp)
    apply auto
@@ -815,6 +815,7 @@ lemma wpc_helper_corres_final:
 
 wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' m f'" wpc_helper_corres_final
 wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' (m >>= f) f'" wpc_helper_corres_final
+wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' (m >>=E f) f'" wpc_helper_corres_final
 
 lemma condition_const: "condition (\<lambda>_. P) L R = (if P then L else R)"
   by (simp add: condition_def split: if_splits)
diff --git a/proof/crefine/lib/Ctac.thy b/proof/crefine/lib/Ctac.thy
index 4de8f947e..b4b82ed2f 100644
--- a/proof/crefine/lib/Ctac.thy
+++ b/proof/crefine/lib/Ctac.thy
@@ -1858,11 +1858,10 @@ method_setup ctac_print_xf = \<open>CtacImpl.corres_print_xf\<close>
   "Print out what ctac thinks is the current xf"
 
 (* Set up wpc *)
-lemma
-  wpc_helper_ccorres_final:
-  "ccorres_underlying sr G rv xf arrel axf Q Q' hs f f'
-   \<Longrightarrow> wpc_helper (P, P') (Q, Q')
-                  (ccorres_underlying sr G rv xf arrel axf P P' hs f f')"
+lemma wpc_helper_ccorres_final:
+  "ccorres_underlying sr G rv xf arrel axf Q Q'' hs f f'
+   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'')
+                  (ccorres_underlying sr G rv xf arrel axf P P'' hs f f')"
   apply (clarsimp simp: wpc_helper_def)
   apply (erule ccorres_guard_imp)
    apply auto
@@ -1870,6 +1869,7 @@ lemma
 
 wpc_setup "\<lambda>m. ccorres_underlying sr G rv xf arrel axf P P' hs m conc" wpc_helper_ccorres_final
 wpc_setup "\<lambda>m. ccorres_underlying sr G rv xf arrel axf P P' hs (m >>= a) conc" wpc_helper_ccorres_final
+wpc_setup "\<lambda>m. ccorres_underlying sr G rv xf arrel axf P P' hs (m >>=E a) conc" wpc_helper_ccorres_final
 
 context kernel
 begin
diff --git a/proof/drefine/Corres_D.thy b/proof/drefine/Corres_D.thy
index 17afc63fa..ecc31e264 100644
--- a/proof/drefine/Corres_D.thy
+++ b/proof/drefine/Corres_D.thy
@@ -244,7 +244,7 @@ lemma dcorres_gets_the:
 
 lemma wpc_helper_dcorres:
   "dcorres r Q Q' f f'
-   \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (dcorres r P (\<lambda>s. s \<in> P') f f')"
+   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (dcorres r P P' f f')"
   apply (clarsimp simp: wpc_helper_def)
   apply (erule corres_guard_imp)
    apply simp
diff --git a/proof/invariant-abstract/AARCH64/Machine_AI.thy b/proof/invariant-abstract/AARCH64/Machine_AI.thy
index b34a001a7..3e7caa4d5 100644
--- a/proof/invariant-abstract/AARCH64/Machine_AI.thy
+++ b/proof/invariant-abstract/AARCH64/Machine_AI.thy
@@ -19,7 +19,7 @@ definition
   "no_irq f \<equiv> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
 
 lemma wpc_helper_no_irq:
-  "no_irq f \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (no_irq f)"
+  "no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)"
   by (simp add: wpc_helper_def)
 
 wpc_setup "\<lambda>m. no_irq m" wpc_helper_no_irq
diff --git a/proof/invariant-abstract/ARM/Machine_AI.thy b/proof/invariant-abstract/ARM/Machine_AI.thy
index ab23862c3..ba4431360 100644
--- a/proof/invariant-abstract/ARM/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM/Machine_AI.thy
@@ -17,7 +17,7 @@ definition
   "no_irq f \<equiv> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
 
 lemma wpc_helper_no_irq:
-  "no_irq f \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (no_irq f)"
+  "no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)"
   by (simp add: wpc_helper_def)
 
 wpc_setup "\<lambda>m. no_irq m" wpc_helper_no_irq
diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
index 13a1f6873..d07aa28bd 100644
--- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
@@ -17,7 +17,7 @@ definition
   "no_irq f \<equiv> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
 
 lemma wpc_helper_no_irq:
-  "no_irq f \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (no_irq f)"
+  "no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)"
   by (simp add: wpc_helper_def)
 
 wpc_setup "\<lambda>m. no_irq m" wpc_helper_no_irq
diff --git a/proof/invariant-abstract/RISCV64/Machine_AI.thy b/proof/invariant-abstract/RISCV64/Machine_AI.thy
index 1aef2e7d5..61fd9255b 100644
--- a/proof/invariant-abstract/RISCV64/Machine_AI.thy
+++ b/proof/invariant-abstract/RISCV64/Machine_AI.thy
@@ -17,7 +17,7 @@ definition
   "no_irq f \<equiv> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
 
 lemma wpc_helper_no_irq:
-  "no_irq f \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (no_irq f)"
+  "no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)"
   by (simp add: wpc_helper_def)
 
 wpc_setup "\<lambda>m. no_irq m" wpc_helper_no_irq
diff --git a/proof/invariant-abstract/X64/Machine_AI.thy b/proof/invariant-abstract/X64/Machine_AI.thy
index 4e37700a4..deae79469 100644
--- a/proof/invariant-abstract/X64/Machine_AI.thy
+++ b/proof/invariant-abstract/X64/Machine_AI.thy
@@ -17,7 +17,7 @@ definition
   "no_irq f \<equiv> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
 
 lemma wpc_helper_no_irq:
-  "no_irq f \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (no_irq f)"
+  "no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)"
   by (simp add: wpc_helper_def)
 
 wpc_setup "\<lambda>m. no_irq m" wpc_helper_no_irq
diff --git a/sys-init/DuplicateCaps_SI.thy b/sys-init/DuplicateCaps_SI.thy
index 2b2361889..24737e6ba 100644
--- a/sys-init/DuplicateCaps_SI.thy
+++ b/sys-init/DuplicateCaps_SI.thy
@@ -256,7 +256,7 @@ lemma distinct_card':
 (* FIXME, move higher *)
 lemma distinct_length_filter':
   "distinct xs \<Longrightarrow> length [x\<leftarrow>xs. P x] = card {x \<in> set xs. P x}"
-  by (metis distinct_length_filter set_conj_Int_simp inf_commute)
+  by (metis distinct_card' distinct_filter set_filter)
 
 lemma duplicate_caps_sep_no_rv:
   "\<lbrace>\<guillemotleft>si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*