removed debugging facilities accidentally left in the committed code
authorboehmes
Wed, 20 Jul 2011 15:09:53 +0200
changeset 43932 b2218b8265ea
parent 43931 c92df8144681
child 43933 6cc1875cf35d
removed debugging facilities accidentally left in the committed code
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')