# HG changeset patch
# User blanchet
# Date 1361371431 -3600
# Node ID 3fba6741ead2dffc1f8593abcbd22fa256d931e5
# Parent  265dca70d8b545b2e41e54edcfebcaccab3ce303
improved hack

diff -r 265dca70d8b5 -r 3fba6741ead2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 20 15:26:19 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 20 15:43:51 2013 +0100
@@ -50,7 +50,7 @@
 
 (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
 (*defaults used in this Mirabelle action*)
-val preplay_timeout_default = "4"
+val preplay_timeout_default = "3"
 val lam_trans_default = "smart"
 val uncurried_aliases_default = "smart"
 val fact_filter_default = "smart"
@@ -383,12 +383,13 @@
 
 type stature = ATP_Problem_Generate.stature
 
-(* hack *)
+(* 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 then
+    if (String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg)
+       andalso not (String.isSubstring "(> " msg) then
       "none" (* trust the preplayed proof *)
     else if String.isSubstring "metis (" msg then
       msg |> Substring.full