src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
changeset 69989 bcba61d92558
parent 67399 eab6ce8368fa
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 26 13:25:32 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 26 13:45:46 2019 +0100
@@ -931,7 +931,6 @@
 fun biggest_hyp_first_tac i = fn st =>
   let
     val results = TERMFUN biggest_hypothesis (SOME i) st
-val _ = tracing ("result=" ^ @{make_string} results)
   in
     if null results then no_tac st
     else