src/HOL/Tools/ATP_Manager/atp_minimal.ML

 Minimalization of theorem list for metis by using an external automated theorem prover
 *)
 
 signature ATP_MINIMAL =
 sig
-  val minimalize: AtpWrapper.prover -> string -> int -> Proof.state ->
+  val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
     (string * thm list) list -> ((string * thm list) list * int) option * string
 end
 
-structure AtpMinimal: ATP_MINIMAL =
+structure ATP_Minimal: ATP_MINIMAL =
 struct
 
 (* output control *)
 
 fun debug str = Output.debug (fn () => str)

    ("# Cannot determine problem status within resource limit", Timeout),
    ("Error", Error)]
 
 fun produce_answer result =
   let
-    val AtpWrapper.Prover_Result {success, message, proof=result_string,
+    val ATP_Wrapper.Prover_Result {success, message, proof=result_string,
       internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result
   in
   if success then
     (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
   else

       else
         (Failure, result_string)
     end
   end
 
+
 (* wrapper for calling external prover *)
 
 fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
   let
     val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val _ = debug_fn (fn () => print_names name_thm_pairs)
     val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
-    val problem = AtpWrapper.ATP_Problem {
-      with_full_types = AtpManager.get_full_types (),
+    val problem = ATP_Wrapper.ATP_Problem {
+      with_full_types = ATP_Manager.get_full_types (),
       subgoal = subgoalno,
       goal = Proof.get_goal state,
       axiom_clauses = SOME axclauses,
       filtered_clauses = filtered }
     val (result, proof) = produce_answer (prover problem time_limit)

 
 fun sh_min_command args thm_names state =
   let
     val (prover_name, time_limit) = get_options args
     val prover =
-      case AtpManager.get_prover prover_name (Proof.theory_of state) of
+      case ATP_Manager.get_prover prover_name (Proof.theory_of state) of
         SOME prover => prover
       | NONE => error ("Unknown prover: " ^ quote prover_name)
     val name_thms_pairs = get_thms (Proof.context_of state) thm_names
     fun print_answer (_, msg) = answer msg
   in