src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 55275 e1bf9f0c5420
parent 55274 b84867d6550b
child 55279 df41d34d1324
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -314,7 +314,6 @@
           |> tap (trace_isar_proof "Original")
           |> compress_isar_proof ctxt compress_isar preplay_data
           |> tap (trace_isar_proof "Compressed")
-          |> tap (trace_isar_proof "Tried0")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)