prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc.

--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun Aug 22 08:30:19 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun Aug 22 09:43:10 2010 +0200
@@ -22,7 +22,7 @@
   val timestamp : unit -> string
   val is_tptp_variable : string -> bool
   val strings_for_tptp_problem :
-    (string * string problem_line list) list -> string list
+    bool -> (string * string problem_line list) list -> string list
   val nice_tptp_problem :
     bool -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
@@ -48,6 +48,10 @@
 
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
+fun string_for_kind Axiom = "axiom"
+  | string_for_kind Hypothesis = "hypothesis"
+  | string_for_kind Conjecture = "conjecture"
+
 fun string_for_term (ATerm (s, [])) = s
   | string_for_term (ATerm ("equal", ts)) =
     space_implode " = " (map string_for_term ts)
@@ -74,20 +78,26 @@
                         (map string_for_formula phis) ^ ")"
   | string_for_formula (AAtom tm) = string_for_term tm
 
-fun string_for_problem_line (Fof (ident, kind, phi)) =
-  "fof(" ^ ident ^ ", " ^
-  (case kind of
-     Axiom => "axiom"
-   | Hypothesis => "hypothesis"
-   | Conjecture => "conjecture") ^
-  ",\n    (" ^ string_for_formula phi ^ ")).\n"
-fun strings_for_tptp_problem problem =
+fun string_for_problem_line use_conjecture_for_hypotheses
+                            (Fof (ident, kind, phi)) =
+  let
+    val (kind, phi) =
+      if kind = Hypothesis andalso use_conjecture_for_hypotheses then
+        (Conjecture, AConn (ANot, [phi]))
+      else
+        (kind, phi)
+  in
+    "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
+    string_for_formula phi ^ ")).\n"
+  end
+fun strings_for_tptp_problem use_conjecture_for_hypotheses problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
   maps (fn (_, []) => []
          | (heading, lines) =>
            "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
-           map string_for_problem_line lines) problem
+           map (string_for_problem_line use_conjecture_for_hypotheses) lines)
+       problem
 
 fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
 

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Aug 22 08:30:19 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Aug 22 09:43:10 2010 +0200
@@ -20,7 +20,8 @@
      known_failures: (failure * string) list,
      default_max_relevant_per_iter: int,
      default_theory_relevant: bool,
-     explicit_forall: bool}
+     explicit_forall: bool,
+     use_conjecture_for_hypotheses: bool}
 
   val string_for_failure : failure -> string
   val known_failure_in_output :
@@ -51,7 +52,8 @@
    known_failures: (failure * string) list,
    default_max_relevant_per_iter: int,
    default_theory_relevant: bool,
-   explicit_forall: bool}
+   explicit_forall: bool,
+   use_conjecture_for_hypotheses: bool}
 
 val missing_message_tail =
   " appears to be missing. You will need to install it if you want to run \
@@ -146,7 +148,8 @@
       (OutOfResources, "SZS status ResourceOut")],
    default_max_relevant_per_iter = 50 (* FIXME *),
    default_theory_relevant = false,
-   explicit_forall = false}
+   explicit_forall = false,
+   use_conjecture_for_hypotheses = true}
 
 val e = ("e", e_config)
 
@@ -173,7 +176,8 @@
       (SpassTooOld, "tptp2dfg")],
    default_max_relevant_per_iter = 35 (* FIXME *),
    default_theory_relevant = true,
-   explicit_forall = true}
+   explicit_forall = true,
+   use_conjecture_for_hypotheses = true}
 
 val spass = ("spass", spass_config)
 
@@ -199,7 +203,8 @@
       (VampireTooOld, "not a valid option")],
    default_max_relevant_per_iter = 45 (* FIXME *),
    default_theory_relevant = false,
-   explicit_forall = false}
+   explicit_forall = false,
+   use_conjecture_for_hypotheses = true}
 
 val vampire = ("vampire", vampire_config)
 
@@ -230,7 +235,8 @@
   | SOME sys => sys);
 
 fun remote_config system_prefix proof_delims known_failures
-                  default_max_relevant_per_iter default_theory_relevant =
+                  default_max_relevant_per_iter default_theory_relevant
+                  use_conjecture_for_hypotheses =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
@@ -242,20 +248,25 @@
      [(TimedOut, "says Timeout")],
    default_max_relevant_per_iter = default_max_relevant_per_iter,
    default_theory_relevant = default_theory_relevant,
-   explicit_forall = true}
+   explicit_forall = true,
+   use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
 
 fun remotify_config system_prefix
         ({proof_delims, known_failures, default_max_relevant_per_iter,
-          default_theory_relevant, ...} : prover_config) : prover_config =
+          default_theory_relevant, use_conjecture_for_hypotheses, ...}
+         : prover_config) : prover_config =
   remote_config system_prefix proof_delims known_failures
                 default_max_relevant_per_iter default_theory_relevant
+                use_conjecture_for_hypotheses
 
 val remotify_name = prefix "remote_"
 fun remote_prover name system_prefix proof_delims known_failures
-                  default_max_relevant_per_iter default_theory_relevant =
+                  default_max_relevant_per_iter default_theory_relevant
+                  use_conjecture_for_hypotheses =
   (remotify_name name,
    remote_config system_prefix proof_delims known_failures
-                 default_max_relevant_per_iter default_theory_relevant)
+                 default_max_relevant_per_iter default_theory_relevant
+                 use_conjecture_for_hypotheses)
 fun remotify_prover (name, config) system_prefix =
   (remotify_name name, remotify_config system_prefix config)
 
@@ -263,10 +274,10 @@
 val remote_vampire = remotify_prover vampire "Vampire---9"
 val remote_sine_e =
   remote_prover "sine_e" "SInE---" []
-                [(Unprovable, "says Unknown")] 150 (* FIXME *) false
+                [(Unprovable, "says Unknown")] 150 (* FIXME *) false true
 val remote_snark =
   remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
-                50 (* FIXME *) false
+                50 (* FIXME *) false true
 
 (* Setup *)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 22 08:30:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 22 09:43:10 2010 +0200
@@ -209,7 +209,7 @@
 fun prover_fun atp_name
         {exec, required_execs, arguments, proof_delims, known_failures,
          default_max_relevant_per_iter, default_theory_relevant,
-         explicit_forall}
+         explicit_forall, use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           relevance_threshold, relevance_convergence,
           max_relevant_per_iter, theory_relevant,
@@ -309,7 +309,9 @@
             val (problem, pool, conjecture_offset, axiom_names) =
               prepare_problem ctxt readable_names explicit_forall full_types
                               explicit_apply hyp_ts concl_t the_axioms
-            val _ = File.write_list probfile (strings_for_tptp_problem problem)
+            val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
+                                              problem
+            val _ = File.write_list probfile ss
             val conjecture_shape =
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
               |> map single