--- 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