1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 09 04:44:59 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 09 05:06:48 2013 +0100
     1.3 @@ -336,7 +336,13 @@
     1.4            #> relabel_proof
     1.5          val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
     1.6            refute_graph
     1.7 +(*
     1.8 +          |> tap (tracing o prefix "REFUTE: " o string_of_refute_graph)
     1.9 +*)
    1.10            |> redirect_graph axioms tainted bot
    1.11 +(*
    1.12 +          |> tap (tracing o prefix "DIRECT: " o string_of_direct_proof)
    1.13 +*)
    1.14            |> isar_proof_of_direct_proof
    1.15            |> relabel_proof_canonically
    1.16            |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay