diff -r 988d7c7e2254 -r 7ff39293e265 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Feb 07 15:26:22 2022 +0100
@@ -314,9 +314,11 @@
         original @ shifted_once @ shifted_twice
       end
 
-    fun adjust_extra (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0) =
-      (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
-       the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
+    fun adjust_extra (ATP_Slice (format0, type_enc0, lam_trans0, uncurried_aliases0,
+        extra_extra0)) =
+        ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
+          the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
+      | adjust_extra (extra as SMT_Slice _) = extra
 
     fun adjust_slice ((num_facts0, fact_filter0), extra) =
       let
@@ -324,7 +326,7 @@
         val max_facts = max_facts |> the_default num_facts0
         val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
       in
-        ((num_facts, fact_filter), Option.map adjust_extra extra)
+        ((num_facts, fact_filter), adjust_extra extra)
       end
 
     val provers = distinct (op =) schedule