--- 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
--- 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