# HG changeset patch
# User blanchet
# Date 1280246310 -7200
# Node ID d9c4d87838f31a1338026fc005b95c0d24a98515
# Parent  e024504943d1d60751ee6862e3cc61559cb04f6d
kill needless tracing

diff -r e024504943d1 -r d9c4d87838f3 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:56:01 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:58:30 2010 +0200
@@ -7,7 +7,6 @@
 
 signature ATP_SYSTEMS =
 sig
-  val trace : bool Unsynchronized.ref
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_runtime : bool Config.T
@@ -26,9 +25,6 @@
 open Sledgehammer_Proof_Reconstruct
 open Sledgehammer
 
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if !trace then tracing (msg ()) else ()
-
 (** generic ATP **)
 
 (* external problem files *)
@@ -308,7 +304,6 @@
     val thy = ProofContext.theory_of ctxt
     val goal_t = Logic.list_implies (hyp_ts, concl_t)
     val is_FO = Meson.is_fol_term thy goal_t
-    val _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t)
     val axtms = map (prop_of o snd) extra_cls
     val subs = tfree_classes_of_terms [goal_t]
     val supers = tvar_classes_of_terms axtms