compile
authorblanchet
Wed, 23 Nov 2022 11:48:07 +0100
changeset 76525 eb294dd8e266
parent 76524 87217c655984
child 76526 33025e13dcdc
compile
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 ^ ")")