From 8dd5dfe5a9678d83decd643eeda020d2dbd11c47 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Thu, 8 Aug 2024 20:04:11 +0930
Subject: [PATCH] fixup crunch again squash

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 proof/refine/RISCV64/IpcCancel_R.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy
index ed02829345..f0ac9a59df 100644
--- 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>