# HG changeset patch
# User blanchet
# Date 1643715153 -3600
# Node ID 1a8f6cb5efd602477b02b29a5e3808a697b4eb4e
# Parent  632c9ae415fac32f5a3d7c2b5a7297c814907f66
don't perform preplaying steps if preplaying is disabled

diff -r 632c9ae415fa -r 1a8f6cb5efd6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 01 12:14:43 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 01 12:32:33 2022 +0100
@@ -450,7 +450,7 @@
               |> compress_isar_proof ctxt compress preplay_timeout preplay_data
               |> tap (trace_isar_proof "Compressed")
               |> postprocess_isar_proof_remove_unreferenced_steps
-                   (keep_fastest_method_of_isar_step (!preplay_data)
+                   (do_preplay ? keep_fastest_method_of_isar_step (!preplay_data)
                     #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
               |> tap (trace_isar_proof "Minimized")
               |> `(preplay_outcome_of_isar_proof (!preplay_data))