# HG changeset patch
# User blanchet
# Date 1283516447 -7200
# Node ID 240e2b41a041e238b7a0fd2516700e485157c99a
# Parent  91ba394cc5258625506cbcf6fe0a7301f2df5b82
remove code I submitted accidentally

diff -r 91ba394cc525 -r 240e2b41a041 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Sep 03 13:54:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Sep 03 14:20:47 2010 +0200
@@ -798,7 +798,6 @@
     val thy = ProofContext.theory_of ctxt
     val _ = trace_msg (fn () =>
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
-val timer = Timer.startRealTimer () (*###*)
   in
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
@@ -807,9 +806,6 @@
                   (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
-|> tap (fn _ => priority (" METIS " ^
-cat_lines (map (Display.string_of_thm ctxt) ths) ^
-string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ " ms")) (*###*)
   end
 
 val metis_tac = generic_metis_tac HO