diff -r 787b69fffaae -r 46a94aa3ec8e src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jan 31 16:09:23 2022 +0100
@@ -14,8 +14,8 @@
 imports Type_Encodings
 begin
 
-sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
-  dont_minimize]
+sledgehammer_params [prover = spass, fact_filter = mepo, slices = 1, timeout = 30,
+  preplay_timeout = 0, dont_minimize]
 
 text \<open>Extensionality and set constants\<close>