# HG changeset patch
# User blanchet
# Date 1321391619 -3600
# Node ID 96696c360b3eebab51b7f7bdebb78ca98c6629f4
# Parent  624872fc47bfdfa46a5019da9356ed43ca32bb76
disable debugging output

diff -r 624872fc47bf -r 96696c360b3e src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:13:39 2011 +0100
@@ -227,8 +227,10 @@
     val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
                           false preproc [] @{prop False} props
+    (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (lines_for_atp_problem CNF atp_problem))
+    *)
     (* "rev" is for compatibility with existing proof scripts. *)
     val axioms =
       atp_problem