--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 20 14:44:00 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 20 14:47:19 2013 +0100
@@ -388,7 +388,9 @@
(case AList.lookup (op =) args reconstructorK of
SOME name => name
| NONE =>
- if String.isSubstring "metis (" msg then
+ if String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg then
+ "none" (* trust the preplayed proof *)
+ else if String.isSubstring "metis (" msg then
msg |> Substring.full
|> Substring.position "metis ("
|> snd |> Substring.position ")"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:44:00 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:47:19 2013 +0100
@@ -807,18 +807,16 @@
| _ =>
let
val msg =
+ (if verbose then
+ let
+ val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
+ in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
+ else
+ []) @
(if preplay then
[(if preplay_fail then "may fail, " else "") ^
Sledgehammer_Preplay.string_of_preplay_time preplay_time]
else
- []) @
- (if verbose then
- let
- val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
- in
- [string_of_int num_steps ^ " step" ^ plural_s num_steps]
- end
- else
[])
in
"\n\nStructured proof "