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