natural argument order for prover;
renamed atp_problem to problem;
standard naming convention for the_system;

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 15 17:06:19 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 15 17:49:30 2009 +0200
@@ -301,14 +301,14 @@
     val (ctxt, goal) = Proof.get_goal st
     val ctxt' = if is_none dir then ctxt
       else Config.put ATP_Wrapper.destdir (the dir) ctxt
-    val atp = prover (ATP_Wrapper.atp_problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal))
+    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal);
 
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) =
-      time_limit (Mirabelle.cpu_time atp) timeout
+      time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
   in
     if success then (message, SH_OK (time_isa, time_atp, theorem_names))
     else (message, SH_FAIL(time_isa, time_atp))

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 17:06:19 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 17:49:30 2009 +0200
@@ -323,9 +323,9 @@
           let
             val _ = register birthtime deadtime (Thread.self (), desc);
             val problem =
-              ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state);
+              ATP_Wrapper.problem_of_goal (! full_types) i (Proof.get_goal proof_state);
             val result =
-              let val {success, message, ...} = prover problem (! timeout);
+              let val {success, message, ...} = prover (! timeout) problem;
               in (success, message) end
               handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
                   (true, "Empty clause: Try this command: " ^

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 15 17:06:19 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 15 17:49:30 2009 +0200
@@ -110,7 +110,7 @@
       goal = Proof.get_goal state,
       axiom_clauses = SOME axclauses,
       filtered_clauses = filtered}
-    val (result, proof) = produce_answer (prover problem time_limit)
+    val (result, proof) = produce_answer (prover time_limit problem)
     val _ = priority (string_of_result result)
   in
     (result, proof)

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 15 17:06:19 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 15 17:49:30 2009 +0200
@@ -18,13 +18,13 @@
     max_new_clauses: int,
     insert_theory_const: bool,
     emit_structured_proof: bool}
-  type atp_problem =
+  type problem =
    {with_full_types: bool,
     subgoal: int,
     goal: Proof.context * (thm list * thm),
     axiom_clauses: (thm * (string * int)) list option,
     filtered_clauses: (thm * (string * int)) list option}
-  val atp_problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> atp_problem
+  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
   type prover_result =
    {success: bool,
     message: string,
@@ -33,7 +33,7 @@
     proof: string,
     internal_thm_names: string Vector.vector,
     filtered_clauses: (thm * (string * int)) list}
-  type prover = atp_problem -> int -> prover_result
+  type prover = int -> problem -> prover_result
 
   (*common provers*)
   val vampire: string * prover
@@ -73,14 +73,14 @@
   insert_theory_const: bool,
   emit_structured_proof: bool};
 
-type atp_problem =
+type problem =
  {with_full_types: bool,
   subgoal: int,
   goal: Proof.context * (thm list * thm),
   axiom_clauses: (thm * (string * int)) list option,
   filtered_clauses: (thm * (string * int)) list option};
 
-fun atp_problem_of_goal with_full_types subgoal goal : atp_problem =
+fun problem_of_goal with_full_types subgoal goal : problem =
  {with_full_types = with_full_types,
   subgoal = subgoal,
   goal = goal,
@@ -96,7 +96,7 @@
   internal_thm_names: string Vector.vector,
   filtered_clauses: (thm * (string * int)) list};
 
-type prover = atp_problem -> int -> prover_result;
+type prover = int -> problem -> prover_result;
 
 
 (* basic template *)
@@ -185,7 +185,7 @@
 
 (* generic TPTP-based provers *)
 
-fun gen_tptp_prover (name, prover_config) problem timeout =
+fun gen_tptp_prover (name, prover_config) timeout problem =
   let
     val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
       prover_config;
@@ -262,7 +262,7 @@
   insert_theory_const = insert_theory_const,
   emit_structured_proof = false};
 
-fun gen_dfg_prover (name, prover_config: prover_config) problem timeout =
+fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
   let
     val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config
     val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
@@ -306,7 +306,7 @@
   (if null systems then get_systems () else systems)
   |> `(find_first (String.isPrefix prefix)));
 
-fun get_the_system prefix =
+fun the_system prefix =
   (case get_system prefix of
     NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP")
   | SOME sys => sys);
@@ -314,7 +314,7 @@
 fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
  {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
   arguments =
-    (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ get_the_system prover_prefix),
+    (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
   max_new_clauses = max_new,
   insert_theory_const = insert_tc,
   emit_structured_proof = false};