src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 36231 bede2d49ba3b
parent 36229 c95fab3f9cc5
child 36235 61159615a0c5
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 18:14:45 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 18:44:12 2010 +0200
@@ -35,7 +35,6 @@
   type prover_result =
     {success: bool,
      message: string,
-     conjecture_pos: int * int,
      relevant_thm_names: string list,
      atp_run_time_in_msecs: int,
      proof: string,
@@ -92,7 +91,6 @@
 type prover_result =
   {success: bool,
    message: string,
-   conjecture_pos: int * int,
    relevant_thm_names: string list,
    atp_run_time_in_msecs: int,
    proof: string,