# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID f42fd9754724ff66767e32bf63225f40c2af3002
# Parent  c8b1d9ee375883bbbad105f479eef714aa8a9aad
fixed conjecture resolution bug for Vampire 1.0's TSTP output

diff -r c8b1d9ee3758 -r f42fd9754724 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
@@ -127,7 +127,7 @@
 
 val vampire_step_prefix = "f" (* grrr... *)
 
-fun resolve_fact type_sys _ fact_names ((_, SOME s)) =
+fun resolve_fact type_sys _ fact_names (_, SOME s) =
     (case try (unprefix fact_prefix) s of
        SOME s' =>
        let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in
@@ -147,15 +147,20 @@
       end
     | NONE => []
 
-fun resolve_conjecture conjecture_shape (num, s_opt) =
-  let
-    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
-              SOME s => Int.fromString s |> the_default ~1
-            | NONE => case Int.fromString num of
-                        SOME j => find_index (exists (curry (op =) j))
-                                             conjecture_shape
-                      | NONE => ~1
-  in if k >= 0 then [k] else [] end
+fun resolve_conjecture _ (_, SOME s) =
+    (case try (unprefix conjecture_prefix) s of
+       SOME s' =>
+       (case Int.fromString s' of
+          SOME j => [j]
+        | NONE => [])
+     | NONE => [])
+  | resolve_conjecture conjecture_shape (num, NONE) =
+    case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
+      SOME i =>
+      (case find_index (exists (curry (op =) i)) conjecture_shape of
+         ~1 => []
+       | j => [j])
+    | NONE => []
 
 fun is_fact type_sys conjecture_shape =
   not o null o resolve_fact type_sys 0 conjecture_shape