1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 19 15:45:45 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 19 16:48:50 2013 +0100
     1.3 @@ -838,9 +838,10 @@
     1.4                      Output.urgent_message "Generating proof text..."
     1.5                    else
     1.6                      ()
     1.7 +                val atp_proof = (fn () => termify_atp_proof ctxt pool lifted sym_tab atp_proof)
     1.8                  val isar_params =
     1.9 -                  (debug, verbose, preplay_timeout, isar_compress, isar_try0,
    1.10 -                   pool, fact_names, lifted, sym_tab, atp_proof, goal)
    1.11 +                  (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof,
    1.12 +                   goal)
    1.13                  val one_line_params =
    1.14                    (preplay, proof_banner mode name, used_facts,
    1.15                     choose_minimize_command ctxt params minimize_command name