# HG changeset patch
# User blanchet
# Date 1361368039 -3600
# Node ID 4c6ae305462e7580c9e7cde7f78dadce210a5361
# Parent  3278cd5de3b113dff1a8b256ec2ebb417a7db655
trust preplayed proof in Mirabelle

diff -r 3278cd5de3b1 -r 4c6ae305462e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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 ")"
diff -r 3278cd5de3b1 -r 4c6ae305462e src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 "