diff -r 2168126446bb -r 12de57c5eee5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 13 16:31:01 2012 +0200
@@ -22,7 +22,6 @@
           * (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
-     conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      best_slices :
        Proof.context -> (real * (bool * (slice_spec * string))) list}
@@ -59,7 +58,7 @@
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> formula_kind -> formula_kind
+    -> (failure * string) list -> formula_kind
     -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
   val add_atp : string * (unit -> atp_config) -> theory -> theory
   val get_atp : theory -> string -> (unit -> atp_config)
@@ -90,7 +89,6 @@
         * (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
-   conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
    best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
 
@@ -196,7 +194,6 @@
      [(ProofMissing, ": Valid"),
       (TimedOut, ": Timeout"),
       (GaveUp, ": Unknown")],
-   conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
@@ -304,7 +301,6 @@
      known_szs_status_failures @
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded")],
-   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      let val heuristic = effective_e_selection_heuristic ctxt in
@@ -336,7 +332,6 @@
      known_szs_status_failures @
      [(TimedOut, "CPU time limit exceeded, terminating"),
       (GaveUp, "No.of.Axioms")],
-   conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -361,7 +356,6 @@
    proof_delims =
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    known_failures = known_szs_status_failures,
-   conj_sym_kind = Axiom,
    prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    best_slices =
      (* FUDGE *)
@@ -395,7 +389,6 @@
       (MalformedInput, "Free Variable"),
       (Unprovable, "No formulae and clauses found in input file"),
       (InternalError, "Please report this error")],
-   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -421,7 +414,6 @@
      |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = #proof_delims spass_old_config,
    known_failures = #known_failures spass_old_config,
-   conj_sym_kind = #conj_sym_kind spass_old_config,
    prem_kind = #prem_kind spass_old_config,
    best_slices = fn _ =>
      (* FUDGE *)
@@ -470,7 +462,6 @@
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (Interrupted, "Aborted by signal SIGINT")],
-   conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -499,7 +490,6 @@
      "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
    known_failures = known_szs_status_failures,
-   conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
@@ -519,7 +509,6 @@
    arguments = K (K (K (K (K "")))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
-   conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      K [(1.0, (false, ((200, format, type_enc,
@@ -572,7 +561,7 @@
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 
 fun remote_config system_name system_versions proof_delims known_failures
-                  conj_sym_kind prem_kind best_slice : atp_config =
+                  prem_kind best_slice : atp_config =
   {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
    required_vars = [],
    arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
@@ -581,21 +570,20 @@
      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
-   conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
    best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
 
 fun remotify_config system_name system_versions best_slice
-        ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
-         : atp_config) : atp_config =
+        ({proof_delims, known_failures, prem_kind, ...} : atp_config)
+        : atp_config =
   remote_config system_name system_versions proof_delims known_failures
-                conj_sym_kind prem_kind best_slice
+                prem_kind best_slice
 
 fun remote_atp name system_name system_versions proof_delims known_failures
-               conj_sym_kind prem_kind best_slice =
+               prem_kind best_slice =
   (remote_prefix ^ name,
-   fn () => remote_config system_name system_versions proof_delims known_failures
-                          conj_sym_kind prem_kind best_slice)
+   fn () => remote_config system_name system_versions proof_delims
+                          known_failures prem_kind best_slice)
 fun remotify_atp (name, config) system_name system_versions best_slice =
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice o config)
@@ -618,21 +606,20 @@
   remotify_atp z3_tptp "Z3" ["3.0"]
       (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_e_sine =
-  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture
+  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
       (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
 val remote_iprover =
-  remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
+  remote_atp iproverN "iProver" [] [] [] Conjecture
       (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
 val remote_iprover_eq =
-  remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
+  remote_atp iprover_eqN "iProver-Eq" [] [] [] Conjecture
       (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
-      [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
+      [("refutation.", "end_refutation.")] [] Hypothesis
       (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
 val remote_e_tofof =
-  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
-      Hypothesis
+  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
       (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
@@ -640,7 +627,7 @@
       [(OutOfResources, "Too many function symbols"),
        (Inappropriate, "****  Unexpected end of file."),
        (Crashed, "Unrecoverable Segmentation Fault")]
-      Hypothesis Hypothesis
+      Hypothesis
       (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
 
 (* Setup *)