src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 38820 db482afec7f0
parent 38813 bd443b426d56
child 38823 968f8cc672cd
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 18 20:53:55 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 19 11:02:59 2010 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4          proof_text isar_proof
     1.5              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
     1.6              (full_types, minimize_command, proof, axiom_names, th, subgoal)
     1.7 -      | SOME failure => (string_for_failure failure ^ "\n", [])
     1.8 +      | SOME failure => (string_for_failure failure, [])
     1.9    in
    1.10      {outcome = outcome, message = message, pool = pool,
    1.11       used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,