1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 13:29:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 15:09:53 2011 +0200
     1.3 @@ -554,11 +554,9 @@
     1.4        ts2
     1.5        |> eta_expand ctxt1 is_fol funcs
     1.6        |> rpair ctxt1
     1.7 -      |>> tap (map (tracing o PolyML.makestring))
     1.8        |-> Lambda_Lifting.lift_lambdas NONE is_binder
     1.9        |-> (fn (ts', defs) => fn ctxt' =>
    1.10            map mk_trigger defs @ ts'
    1.11 -          |> tap (map (tracing o PolyML.makestring))
    1.12            |> intro_explicit_application ctxt' funcs 
    1.13            |> pair ctxt')
    1.14