# HG changeset patch
# User blanchet
# Date 1282125840 -7200
# Node ID 0dabf05fc86bd6b93c05e3983086dce347e6ba38
# Parent  54727b44e277c4e4ce7986c68b750be3217cad93
rename enum values

diff -r 54727b44e277 -r 0dabf05fc86b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 18 12:03:44 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 18 12:04:00 2010 +0200
@@ -8,9 +8,9 @@
 signature ATP_SYSTEMS =
 sig
   datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-    OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
-    MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+    OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
+    MalformedInput | MalformedOutput | UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -40,7 +40,7 @@
 
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-  OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+  SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
   MalformedOutput | UnknownError
 
 type prover_config =
@@ -63,7 +63,7 @@
   | string_for_failure CantConnect = "Can't connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
-  | string_for_failure OldSpass =
+  | string_for_failure SpassTooOld =
     "Isabelle requires a more recent version of SPASS with support for the \
     \TPTP syntax. To install it, download and extract the package \
     \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -72,7 +72,7 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
-  | string_for_failure OldVampire =
+  | string_for_failure VampireTooOld =
     "Isabelle requires a more recent version of Vampire. To install it, follow \
     \the instructions from the Sledgehammer manual (\"isabelle doc\
     \ sledgehammer\")."
@@ -170,7 +170,7 @@
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
-      (OldSpass, "tptp2dfg")],
+      (SpassTooOld, "tptp2dfg")],
    max_new_relevant_facts_per_iter = 35 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
@@ -197,7 +197,7 @@
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found"),
-      (OldVampire, "not a valid option")],
+      (VampireTooOld, "not a valid option")],
    max_new_relevant_facts_per_iter = 45 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}