diff -r b6a18a14cc5c -r e7af132d48fe src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri May 06 13:34:59 2011 +0200
@@ -23,13 +23,11 @@
                * string fo_term option * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
 
-  val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
   val is_atp_variable : string -> bool
-  val tptp_strings_for_atp_problem :
-    formula_kind -> format -> string problem -> string list
+  val tptp_strings_for_atp_problem : format -> string problem -> string list
   val nice_atp_problem :
     bool -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
@@ -49,8 +47,6 @@
   AConn of connective * ('a, 'b, 'c) formula list |
   AAtom of 'c
 
-fun mk_anot phi = AConn (ANot, [phi])
-
 datatype format = Fof | Tff
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
@@ -114,35 +110,27 @@
 val default_source =
   ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
 
-fun string_for_problem_line _ _ (Decl (ident, sym, arg_tys, res_ty)) =
+fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
     "tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     string_for_symbol_type arg_tys res_ty ^ ").\n"
-  | string_for_problem_line hypothesis_kind format
+  | string_for_problem_line format
                             (Formula (ident, kind, phi, source, useful_info)) =
-    let
-      val (kind, phi) =
-        if kind = Hypothesis then
-          (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot)
-        else
-          (kind, phi)
-    in
-      (case format of Fof => "fof" | Tff => "tff") ^
-      "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
-      string_for_formula phi ^ ")" ^
-      (case (source, useful_info) of
-         (NONE, NONE) => ""
-       | (SOME tm, NONE) => ", " ^ string_for_term tm
-       | (_, SOME tm) =>
-         ", " ^ string_for_term (source |> the_default default_source) ^
-         ", " ^ string_for_term tm) ^ ").\n"
-    end
-fun tptp_strings_for_atp_problem hypothesis_kind format problem =
+    (case format of Fof => "fof" | Tff => "tff") ^
+    "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
+    string_for_formula phi ^ ")" ^
+    (case (source, useful_info) of
+       (NONE, NONE) => ""
+     | (SOME tm, NONE) => ", " ^ string_for_term tm
+     | (_, SOME tm) =>
+       ", " ^ string_for_term (source |> the_default default_source) ^
+       ", " ^ string_for_term tm) ^ ").\n"
+fun tptp_strings_for_atp_problem format problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
   maps (fn (_, []) => []
          | (heading, lines) =>
            "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
-           map (string_for_problem_line hypothesis_kind format) lines)
+           map (string_for_problem_line format) lines)
        problem
 
 fun is_atp_variable s = Char.isUpper (String.sub (s, 0))