--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Sep 14 23:37:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Sep 14 23:38:20 2010 +0200
@@ -362,10 +362,12 @@
(* ------------------------------------------------------------------------- *)
(*for debugging only*)
+(*
fun print_thpair (fth,th) =
(trace_msg (fn () => "=============================================");
trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
+*)
fun lookth thpairs (fth : Metis.Thm.thm) =
the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
@@ -828,7 +830,6 @@
fun generic_metis_tac mode ctxt ths i st0 =
let
- val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in