diff -r 2479d541bc61 -r 979a0b37f981 src/HOL/Tools/ATP/atp_problem.ML
--- 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))