1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 20 14:44:00 2013 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 20 14:47:19 2013 +0100
     1.3 @@ -388,7 +388,9 @@
     1.4    (case AList.lookup (op =) args reconstructorK of
     1.5      SOME name => name
     1.6    | NONE =>
     1.7 -    if String.isSubstring "metis (" msg then
     1.8 +    if String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg then
     1.9 +      "none" (* trust the preplayed proof *)
    1.10 +    else if String.isSubstring "metis (" msg then
    1.11        msg |> Substring.full
    1.12            |> Substring.position "metis ("
    1.13            |> snd |> Substring.position ")"

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 14:44:00 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 14:47:19 2013 +0100
     2.3 @@ -807,18 +807,16 @@
     2.4          | _ =>
     2.5            let
     2.6              val msg =
     2.7 +              (if verbose then
     2.8 +                let
     2.9 +                  val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
    2.10 +                in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
    2.11 +               else
    2.12 +                 []) @
    2.13                (if preplay then
    2.14                  [(if preplay_fail then "may fail, " else "") ^
    2.15                     Sledgehammer_Preplay.string_of_preplay_time preplay_time]
    2.16                 else
    2.17 -                 []) @
    2.18 -              (if verbose then
    2.19 -                let
    2.20 -                  val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
    2.21 -                in
    2.22 -                  [string_of_int num_steps ^ " step" ^ plural_s num_steps]
    2.23 -                end
    2.24 -               else
    2.25                   [])
    2.26            in
    2.27              "\n\nStructured proof "