# HG changeset patch
# User blanchet
# Date 1376906733 -7200
# Node ID 2a62d848a56a817db3fc44796ea42c77d3c62bf1
# Parent  d815e25ead03cd636c1617b2002554f224d5a940
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success

diff -r d815e25ead03 -r 2a62d848a56a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Aug 18 23:37:38 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 19 12:05:33 2013 +0200
@@ -383,14 +383,18 @@
 
 type stature = ATP_Problem_Generate.stature
 
+fun good_line s =
+  (String.isSubstring " ms)" s orelse String.isSubstring " s)" s)
+  andalso not (String.isSubstring "(> " s)
+  andalso not (String.isSubstring ", > " s)
+  andalso not (String.isSubstring "may fail" s)
+
 (* Fragile hack *)
 fun reconstructor_from_msg args msg =
   (case AList.lookup (op =) args reconstructorK of
     SOME name => name
   | NONE =>
-    if (String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg)
-       andalso not (String.isSubstring "(> " msg)
-       andalso not (String.isSubstring ", > " msg) then
+    if exists good_line (split_lines msg) then
       "none" (* trust the preplayed proof *)
     else if String.isSubstring "metis (" msg then
       msg |> Substring.full