# HG changeset patch
# User blanchet
# Date 1386562008 -3600
# Node ID 65c4fd04b5b26ed535d1c92eaa66af8ed8101b2f
# Parent  fed04f257898800238d2e4ff054897a57a10dea3
useful debugging info

diff -r fed04f257898 -r 65c4fd04b5b2 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 09 04:44:59 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 09 05:06:48 2013 +0100
@@ -336,7 +336,13 @@
           #> relabel_proof
         val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
           refute_graph
+(*
+          |> tap (tracing o prefix "REFUTE: " o string_of_refute_graph)
+*)
           |> redirect_graph axioms tainted bot
+(*
+          |> tap (tracing o prefix "DIRECT: " o string_of_direct_proof)
+*)
           |> isar_proof_of_direct_proof
           |> relabel_proof_canonically
           |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay