disable debugging output
authorblanchet
Tue Nov 15 22:13:39 2011 +0100 (2011-11-15)
changeset 4551096696c360b3e
parent 45509 624872fc47bf
child 45511 9b0f8ca4388e
disable debugging output
src/HOL/Tools/Metis/metis_translate.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:13:39 2011 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:13:39 2011 +0100
     1.3 @@ -227,8 +227,10 @@
     1.4      val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
     1.5        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
     1.6                            false preproc [] @{prop False} props
     1.7 +    (*
     1.8      val _ = tracing ("ATP PROBLEM: " ^
     1.9                       cat_lines (lines_for_atp_problem CNF atp_problem))
    1.10 +    *)
    1.11      (* "rev" is for compatibility with existing proof scripts. *)
    1.12      val axioms =
    1.13        atp_problem