# HG changeset patch
# User wenzelm
# Date 1553604346 -3600
# Node ID bcba61d925582737d2ae78e10657a95e09317707
# Parent  6fa51a36b7f788e1331db958630fb33613118df0
removed spurious debugging;

diff -r 6fa51a36b7f7 -r bcba61d92558 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Mar 26 13:25:32 2019 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Mar 26 13:45:46 2019 +0100
@@ -53,8 +53,7 @@
   let
     fun tac [] st = all_tac st
       | tac (type_enc :: type_encs) st =
-        st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *)
-           |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1)
+        st |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1)
                THEN Metis_Tactic.metis_tac [type_enc]
                     ATP_Problem_Generate.combsN ctxt ths 1
                THEN COND (has_fewer_prems 2) all_tac no_tac
diff -r 6fa51a36b7f7 -r bcba61d92558 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- 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