# HG changeset patch
# User wenzelm
# Date 1391276447 -3600
# Node ID 7c6c833069d2bfdbbf483d0572d232353fba8560
# Parent  3229614ca9c5c9a2a50d4c4e71d3978016582267
unused;

diff -r 3229614ca9c5 -r 7c6c833069d2 src/HOL/Tools/Metis/metis_reconstruct.ML
--- 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 =>