# HG changeset patch
# User blanchet
# Date 1284976279 -7200
# Node ID f97fa74c388e3fcff4d043ec086c670137f84ed2
# Parent  346f6d79cba664cf02514b9ca93b506d1f05101e
merge tracing of two related modules

diff -r 346f6d79cba6 -r f97fa74c388e src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Sep 20 10:29:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Sep 20 11:51:19 2010 +0200
@@ -11,7 +11,7 @@
 sig
   type mode = Metis_Translate.mode
 
-  val trace: bool Unsynchronized.ref
+  val trace : bool Unsynchronized.ref
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val replay_one_inference :
     Proof.context -> mode -> (string * term) list
diff -r 346f6d79cba6 -r f97fa74c388e src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 10:29:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 11:51:19 2010 +0200
@@ -23,7 +23,6 @@
 open Metis_Translate
 open Metis_Reconstruct
 
-val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);