# HG changeset patch
# User blanchet
# Date 1387461861 -3600
# Node ID 6e78f87ed554cad643fedadd1d378125a79ed87f
# Parent  a80bd631e57309e5fbd490dc2c550fbca605df4b
removed debugging output

diff -r a80bd631e573 -r 6e78f87ed554 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Dec 19 14:57:21 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Dec 19 15:04:21 2013 +0100
@@ -498,7 +498,6 @@
     val thy = Proof_Context.theory_of ctxt
     val t = u
       |> prop_of_atp ctxt true sym_tab
-|> tap (fn t => tracing ("termify_line: " ^ Syntax.string_of_term ctxt t)) (*###*)
       |> uncombine_term thy
       |> unlift_term lifted
       |> infer_formula_types ctxt