diff --git a/proof/refine/ARM/EmptyFail_H.thy b/proof/refine/ARM/EmptyFail_H.thy
index 6f5669262..148de47f6 100644
--- a/proof/refine/ARM/EmptyFail_H.thy
+++ b/proof/refine/ARM/EmptyFail_H.thy
@@ -165,7 +165,10 @@ lemma ignoreFailure_empty_fail[intro!, wp, simp]:
 context
 notes option.case_cong_weak[cong]
 begin
-crunch (empty_fail) empty_fail[intro!, wp, simp]: cancelIPC, setThreadState, tcbSchedDequeue, setupReplyMaster, isStopped, possibleSwitchTo, tcbSchedAppend
+crunch (empty_fail) empty_fail[intro!, wp, simp]:
+  cancelIPC, setThreadState, tcbSchedDequeue, setupReplyMaster, isStopped,
+  possibleSwitchTo, tcbSchedAppend
+  (simp: crunch_simps)
 end
 
 crunch (empty_fail) "_H_empty_fail"[intro!, wp, simp]: "ThreadDecls_H.suspend"