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