removed debugging output
authorblanchet
Thu, 19 Dec 2013 15:04:21 +0100
changeset 54819 6e78f87ed554
parent 54818 a80bd631e573
child 54820 d9ab86c044fd
removed debugging output
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