diff --git a/proof/crefine/ARM/CSpace_RAB_C.thy b/proof/crefine/ARM/CSpace_RAB_C.thy
index eda10c9a3..84412cb53 100644
--- a/proof/crefine/ARM/CSpace_RAB_C.thy
+++ b/proof/crefine/ARM/CSpace_RAB_C.thy
@@ -168,10 +168,8 @@ next
      apply (simp add: cap_get_tag_isCap split del: if_split)
      apply (thin_tac "ret__unsigned = X" for X)
      apply (rule ccorres_split_throws [where P = "?P"])
-      apply (rule_tac G' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
-                              \<inter> {s. unat (n_bits_' s) = guard'})"
-         in ccorres_abstract  [where xf' = w_rightsMask_'])
-       apply (rule ceqv_refl)
+      apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \<inter> {s. unat (n_bits_' s) = guard'}"
+               in ccorres_inst)
       apply (rule_tac r' = "?rvr" in
           ccorres_rel_imp [where xf' = rab_xf])
        defer
diff --git a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy
index 93c935fa8..465923603 100644
--- a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy
+++ b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy
@@ -205,10 +205,8 @@ next
      apply (simp add: cap_get_tag_isCap split del: if_split)
      apply (thin_tac "ret__unsigned = X" for X)
      apply (rule ccorres_split_throws [where P = "?P"])
-      apply (rule_tac G' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
-                              \<inter> {s. unat (n_bits_' s) = guard'})"
-         in ccorres_abstract  [where xf' = w_rightsMask_'])
-       apply (rule ceqv_refl)
+      apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \<inter> {s. unat (n_bits_' s) = guard'}"
+               in ccorres_inst)
       apply (rule_tac r' = "?rvr" in
           ccorres_rel_imp [where xf' = rab_xf])
        defer
diff --git a/proof/crefine/RISCV64/CSpace_RAB_C.thy b/proof/crefine/RISCV64/CSpace_RAB_C.thy
index ef2218fd6..c4c556490 100644
--- a/proof/crefine/RISCV64/CSpace_RAB_C.thy
+++ b/proof/crefine/RISCV64/CSpace_RAB_C.thy
@@ -208,10 +208,8 @@ next
      apply (simp add: cap_get_tag_isCap split del: if_split)
      apply (thin_tac "ret__unsigned_longlong = X" for X)
      apply (rule ccorres_split_throws [where P = "?P"])
-      apply (rule_tac G' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
-                              \<inter> {s. unat (n_bits_' s) = guard'})"
-         in ccorres_abstract  [where xf' = w_rightsMask_'])
-       apply (rule ceqv_refl)
+      apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \<inter> {s. unat (n_bits_' s) = guard'}"
+               in ccorres_inst)
       apply (rule_tac r' = "?rvr" in
           ccorres_rel_imp [where xf' = rab_xf])
        defer
diff --git a/proof/crefine/X64/CSpace_RAB_C.thy b/proof/crefine/X64/CSpace_RAB_C.thy
index ee0ec07e9..c7838029c 100644
--- a/proof/crefine/X64/CSpace_RAB_C.thy
+++ b/proof/crefine/X64/CSpace_RAB_C.thy
@@ -208,10 +208,8 @@ next
      apply (simp add: cap_get_tag_isCap split del: if_split)
      apply (thin_tac "ret__unsigned_longlong = X" for X)
      apply (rule ccorres_split_throws [where P = "?P"])
-      apply (rule_tac G' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
-                              \<inter> {s. unat (n_bits_' s) = guard'})"
-         in ccorres_abstract  [where xf' = w_rightsMask_'])
-       apply (rule ceqv_refl)
+      apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \<inter> {s. unat (n_bits_' s) = guard'}"
+               in ccorres_inst)
       apply (rule_tac r' = "?rvr" in
           ccorres_rel_imp [where xf' = rab_xf])
        defer