1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 20 15:26:19 2013 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 20 15:43:51 2013 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
     1.6  (*defaults used in this Mirabelle action*)
     1.7 -val preplay_timeout_default = "4"
     1.8 +val preplay_timeout_default = "3"
     1.9  val lam_trans_default = "smart"
    1.10  val uncurried_aliases_default = "smart"
    1.11  val fact_filter_default = "smart"
    1.12 @@ -383,12 +383,13 @@
    1.13  
    1.14  type stature = ATP_Problem_Generate.stature
    1.15  
    1.16 -(* hack *)
    1.17 +(* Fragile hack *)
    1.18  fun reconstructor_from_msg args msg =
    1.19    (case AList.lookup (op =) args reconstructorK of
    1.20      SOME name => name
    1.21    | NONE =>
    1.22 -    if String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg then
    1.23 +    if (String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg)
    1.24 +       andalso not (String.isSubstring "(> " msg) then
    1.25        "none" (* trust the preplayed proof *)
    1.26      else if String.isSubstring "metis (" msg then
    1.27        msg |> Substring.full