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