# HG changeset patch
# User blanchet
# Date 1375105324 -7200
# Node ID 4183c32197455adbbb8f29ae11b1d86b08c2cddc
# Parent  d9d90d29860e410fd9d73c4f954c719764aad8cf
simplified Vampire hack -- no need to run it for other ATPs

diff -r d9d90d29860e -r 4183c3219745 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 29 15:30:31 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 29 15:42:04 2013 +0200
@@ -196,15 +196,13 @@
 
 val vampire_fact_prefix = "f"
 
-fun step_name_ord p =
+fun vampire_step_name_ord p =
   let val q = pairself fst p in
-    (* The "unprefix" part is to cope with remote Vampire's output. *)
+    (* The "unprefix" part is to cope with Vampire's output. *)
     case pairself (Int.fromString
                    o perhaps (try (unprefix vampire_fact_prefix))) q of
-      (NONE, NONE) => string_ord q
-    | (NONE, SOME _) => LESS
-    | (SOME _, NONE) => GREATER
-    | (SOME i, SOME j) => int_ord (i, j)
+      (SOME i, SOME j) => int_ord (i, j)
+    | _ => raise Fail "not Vampire"
   end
 
 type 'a step = step_name * formula_role * 'a * string * step_name list
@@ -510,7 +508,7 @@
     | NONE =>
       tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
       |> parse_proof problem
-      |> sort (step_name_ord o pairself #1)
+      |> perhaps (try (sort (vampire_step_name_ord o pairself #1)))
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =