1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 14:44:00 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 14:47:19 2013 +0100
     1.3 @@ -807,18 +807,16 @@
     1.4          | _ =>
     1.5            let
     1.6              val msg =
     1.7 +              (if verbose then
     1.8 +                let
     1.9 +                  val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
    1.10 +                in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
    1.11 +               else
    1.12 +                 []) @
    1.13                (if preplay then
    1.14                  [(if preplay_fail then "may fail, " else "") ^
    1.15                     Sledgehammer_Preplay.string_of_preplay_time preplay_time]
    1.16                 else
    1.17 -                 []) @
    1.18 -              (if verbose then
    1.19 -                let
    1.20 -                  val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
    1.21 -                in
    1.22 -                  [string_of_int num_steps ^ " step" ^ plural_s num_steps]
    1.23 -                end
    1.24 -               else
    1.25                   [])
    1.26            in
    1.27              "\n\nStructured proof "