# HG changeset patch
# User blanchet
# Date 1286015551 -7200
# Node ID 2f7b060d0c8db6343ce8597f52671e9ffa4d90b0
# Parent  721ba2c1a79917f23f00ad8bd87c4cb3b0605354
some Poly/ML-specific debugging code escaped in the wild -- comment it out

diff -r 721ba2c1a799 -r 2f7b060d0c8d src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Oct 01 22:44:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Oct 02 12:32:31 2010 +0200
@@ -182,9 +182,10 @@
         handle Int_Pair_Graph.CYCLES _ =>
                error "Cannot replay Metis proof in Isabelle without axiom of \
                      \choice."
-(* FIXME *)
+(* for debugging:
       val _ = tracing ("SUBSTS: " ^ PolyML.makestring substs)
       val _ = tracing ("ORDERED: " ^ PolyML.makestring ordered_clusters)
+*)
     in
       Goal.prove ctxt [] [] @{prop False}
           (K (cut_rules_tac (map fst axioms) 1