# HG changeset patch
# User boehmes
# Date 1311167393 -7200
# Node ID b2218b8265ea93fce74b503a334b75dedbf290c4
# Parent  c92df8144681537fa810ccb56c23fdcc228e02b7
removed debugging facilities accidentally left in the committed code

diff -r c92df8144681 -r b2218b8265ea src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 13:29:54 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 15:09:53 2011 +0200
@@ -554,11 +554,9 @@
       ts2
       |> eta_expand ctxt1 is_fol funcs
       |> rpair ctxt1
-      |>> tap (map (tracing o PolyML.makestring))
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', defs) => fn ctxt' =>
           map mk_trigger defs @ ts'
-          |> tap (map (tracing o PolyML.makestring))
           |> intro_explicit_application ctxt' funcs 
           |> pair ctxt')