diff -r 988d7c7e2254 -r 7ff39293e265 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 07 15:26:22 2022 +0100
@@ -63,7 +63,11 @@
      factss : (string * fact list) list,
      found_proof : string -> unit}
 
-  type prover_slice = base_slice * atp_slice option
+  datatype prover_slice_extra =
+    ATP_Slice of atp_slice
+  | SMT_Slice of string list
+
+  type prover_slice = base_slice * prover_slice_extra
 
   type prover_result =
     {outcome : atp_failure option,
@@ -176,7 +180,11 @@
    factss : (string * fact list) list,
    found_proof : string -> unit}
 
-type prover_slice = base_slice * atp_slice option
+datatype prover_slice_extra =
+  ATP_Slice of atp_slice
+| SMT_Slice of string list
+
+type prover_slice = base_slice * prover_slice_extra
 
 type prover_result =
   {outcome : atp_failure option,