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