fixup crunch again squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Aug 8, 2024 · 8dd5dfe · 8dd5dfe
1 parent a2c37de
commit 8dd5dfe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy
@@ -1051,7 +1051,7 @@ lemma scReplies_of_scTCB_update[simp]:
 crunch schedContextDonate
   for replies_of': "\<lambda>s. P (replies_of' s)" (* this interfers with list_refs_of_replies' *)
   and scReplies_of[wp]: "\<lambda>s. P' (scReplies_of s)"
-  (simp: crunch_simps wp: crunch_wps updateSchedContext_scReplies_of)
+  (simp: crunch_simps wp: crunch_wps)
 
 lemma updateReply_replyNext_update_None:
   "\<lbrace> \<top> \<rbrace>