# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1690882075 -7200
# Node ID ba2afdd29e1d5f1f22b79d5036d73284f776fd6c
# Parent  2e58b5a3fecff76ae8e74fd09116b207b327bbb1
remove debug printing

diff -r 2e58b5a3fecf -r ba2afdd29e1d src/HOL/Tools/SMT/cvc5_replay_methods.ML
--- a/src/HOL/Tools/SMT/cvc5_replay_methods.ML	Thu Jul 27 07:08:32 2023 +0200
+++ b/src/HOL/Tools/SMT/cvc5_replay_methods.ML	Tue Aug 01 11:27:55 2023 +0200
@@ -108,7 +108,7 @@
      else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution
      else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2
      else if r = Lethe_Proof.hole orelse r = "undefined" then Hole
-     else (@{print} ("maybe unsupported rule", r); Other_Rule r)
+     else Other_Rule r
 
 fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
 let