# HG changeset patch
# User blanchet
# Date 1355786257 -3600
# Node ID 42f3630a6a0ff29cf16140f65da3a27055b8a0db
# Parent  074e937459b6bacd7fcadc9bc107828942da15f4
no need for tracing

diff -r 074e937459b6 -r 42f3630a6a0f src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Mon Dec 17 22:09:48 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Dec 18 00:17:37 2012 +0100
@@ -37,7 +37,7 @@
   let
     val report_path = report_file_name |> Path.explode
     val _ = File.write report_path ""
-    fun print s = (tracing s; File.append report_path (s ^ "\n"))
+    fun print s = File.append report_path (s ^ "\n")
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
       default_params ctxt []
     val prover = hd provers