--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Feb 01 18:22:38 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Feb 01 18:40:47 2014 +0100
@@ -84,14 +84,6 @@
(* FOL step Inference Rules *)
(* ------------------------------------------------------------------------- *)
-(*for debugging only*)
-(*
-fun print_thpair ctxt (fth,th) =
- (trace_msg ctxt (fn () => "=============================================");
- trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
- trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
-*)
-
fun lookth th_pairs fth =
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
handle Option.Option =>