tweaked TPTP formula kind for typing information used in the conjecture

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Jun 19 18:12:49 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Jun 19 18:12:49 2011 +0200
@@ -217,7 +217,7 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>
@@ -257,7 +257,7 @@
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
-   conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
+   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>
@@ -299,7 +299,7 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],
-   conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+   conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>