# HG changeset patch
# User blanchet
# Date 1669200487 -3600
# Node ID eb294dd8e266602fe06bd2c18b4426dd18b16d29
# Parent  87217c65598448af3a0cd37c563d27697f60b9fc
compile

diff -r 87217c655984 -r eb294dd8e266 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Nov 23 11:26:50 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Nov 23 11:48:07 2022 +0100
@@ -340,7 +340,7 @@
             if exhaustive_preplay then
               preplay_results
               |> map
-                (fn (meth, play_outcome, used_facts) =>
+                (fn (meth, (play_outcome, used_facts)) =>
                     "Preplay: " ^
                     Sledgehammer_Proof_Methods.string_of_proof_method (map fst used_facts) meth ^
                     " (" ^ Sledgehammer_Proof_Methods.string_of_play_outcome play_outcome ^ ")")