src/HOL/Tools/Sledgehammer/sledgehammer.ML

         val shifted_twice = shift shifted_once
       in
         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
         val fact_filter = fact_filter |> the_default fact_filter0
         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
     val prover_slices =
       map (fn prover => (prover,