diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy
index 730503ab56..bb467af531 100644
--- a/lib/clib/CCorresLemmas.thy
+++ b/lib/clib/CCorresLemmas.thy
@@ -1204,16 +1204,16 @@ proof -
       apply (insert body_inv(2))[1]
       apply (drule_tac x=new_s in meta_spec)
       apply (drule_tac x=rv in meta_spec)
-      apply (frule_tac s=new_s in ccorres_to_vcg_with_prop')
+      apply (frule_tac s=new_s in ccorres_to_vcg_with_prop)
         using nf apply fastforce
        using body_inv apply fastforce
-      apply (rule_tac Q'="{s'. s' \<in> G' \<and> (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv (xf s') \<and> G rv s)}"
-                   in conseqPost)
-        apply (rule hoarep_conj_lift_pre_fix)
-         apply fastforce
-        apply (simp add: conseq_under_new_pre)
-       apply fastforce
-      apply fastforce
+      apply (rule_tac Q'="{s'. s' \<in> G'
+                               \<and> (\<exists>(rv, s) \<in>fst (B rv new_s). (s, s') \<in> srel \<and> rrel rv (xf s')
+                                                               \<and> G rv s)}"
+                   in conseqPost;
+             fastforce?)
+      apply (rule hoarep_conj_lift_pre_fix;
+             fastforce simp: Collect_mono conseq_under_new_pre)
      apply fastforce
     apply (case_tac xstate; clarsimp)
     apply (frule intermediate_Normal_state[OF _ _ setter_hoarep]; assumption?)