# HG changeset patch
# User blanchet
# Date 1394713093 -3600
# Node ID f8ed378ec45705170cbdba76dd894132151660ed
# Parent  175ac95720d4ea8fa3444e0dc076f112f79cdd4c
removed tracing output

diff -r 175ac95720d4 -r f8ed378ec457 src/HOL/Tools/SMT2/z3_new_proof_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof_replay.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_proof_replay.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -55,7 +55,6 @@
 
 fun replay_thm ctxt assumed nthms
     (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
-(tracing ("replay_thm: " ^ @{make_string} (id, rule) ^ " " ^ Syntax.string_of_term ctxt concl);
   if Z3_New_Proof_Methods.is_assumption rule then
     (case Inttab.lookup assumed id of
       SOME (_, thm) => thm
@@ -63,7 +62,6 @@
   else
     under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt
       (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
-) (*###*)
 
 fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
   let val nthms = map (the o Inttab.lookup proofs) prems