modernized structure names;

--- a/src/HOL/ATP_Linkup.thy	Wed Oct 14 23:13:38 2009 +0200
+++ b/src/HOL/ATP_Linkup.thy	Wed Oct 14 23:44:37 2009 +0200
@@ -96,26 +96,26 @@
 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
 use "Tools/res_atp.ML"
 
-use "Tools/ATP_Manager/atp_wrapper.ML" setup AtpWrapper.setup
+use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup
 use "Tools/ATP_Manager/atp_manager.ML"
 use "Tools/ATP_Manager/atp_minimal.ML"
 
 text {* basic provers *}
-setup {* AtpManager.add_prover AtpWrapper.spass *}
-setup {* AtpManager.add_prover AtpWrapper.vampire *}
-setup {* AtpManager.add_prover AtpWrapper.eprover *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
 
 text {* provers with stuctured output *}
-setup {* AtpManager.add_prover AtpWrapper.vampire_full *}
-setup {* AtpManager.add_prover AtpWrapper.eprover_full *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
 
 text {* on some problems better results *}
-setup {* AtpManager.add_prover AtpWrapper.spass_no_tc *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
 
 text {* remote provers via SystemOnTPTP *}
-setup {* AtpManager.add_prover AtpWrapper.remote_vampire *}
-setup {* AtpManager.add_prover AtpWrapper.remote_spass *}
-setup {* AtpManager.add_prover AtpWrapper.remote_eprover *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
   
 
 

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 14 23:13:38 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 14 23:44:37 2009 +0200
@@ -286,8 +286,8 @@
 
 fun get_atp thy args =
   AList.lookup (op =) args proverK
-  |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
-  |> (fn name => (name, the (AtpManager.get_prover name thy)))
+  |> the_default (hd (space_explode " " (ATP_Manager.get_atps ())))
+  |> (fn name => (name, the (ATP_Manager.get_prover name thy)))
 
 local
 
@@ -300,15 +300,15 @@
   let
     val (ctxt, goal) = Proof.get_goal st
     val ctxt' = if is_none dir then ctxt
-      else Config.put AtpWrapper.destdir (the dir) ctxt
-    val atp = prover (AtpWrapper.atp_problem_of_goal
-      (AtpManager.get_full_types ()) 1 (ctxt', goal))
+      else Config.put ATP_Wrapper.destdir (the dir) ctxt
+    val atp = prover (ATP_Wrapper.atp_problem_of_goal
+      (ATP_Manager.get_full_types ()) 1 (ctxt', goal))
 
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
-    val (AtpWrapper.Prover_Result {success, message, theorem_names,
+    val (ATP_Wrapper.Prover_Result {success, message, theorem_names,
       runtime=time_atp, ...}, time_isa) =
       time_limit (Mirabelle.cpu_time atp) timeout
   in
@@ -372,7 +372,7 @@
   let
     val n0 = length (these (!named_thms))
     val (prover_name, prover) = get_atp (Proof.theory_of st) args
-    val minimize = AtpMinimal.minimalize prover prover_name
+    val minimize = ATP_Minimal.minimalize prover prover_name
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
@@ -448,7 +448,7 @@
 
 fun invoke args =
   let
-    val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
+    val _ = ATP_Manager.set_full_types (AList.defined (op =) args full_typesK)
   in Mirabelle.register (init, sledgehammer_action args, done) end
 
 end

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:13:38 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:44:37 2009 +0200
@@ -21,13 +21,13 @@
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
-  val add_prover: string * AtpWrapper.prover -> theory -> theory
+  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
   val print_provers: theory -> unit
-  val get_prover: string -> theory -> AtpWrapper.prover option
+  val get_prover: string -> theory -> ATP_Wrapper.prover option
   val sledgehammer: string list -> Proof.state -> unit
 end;
 
-structure AtpManager: ATP_MANAGER =
+structure ATP_Manager: ATP_MANAGER =
 struct
 
 (** preferences **)
@@ -302,7 +302,7 @@
 
 structure Provers = TheoryDataFun
 (
-  type T = (AtpWrapper.prover * stamp) Symtab.table
+  type T = (ATP_Wrapper.prover * stamp) Symtab.table
   val empty = Symtab.empty
   val copy = I
   val extend = I
@@ -337,10 +337,10 @@
         val _ = SimpleThread.fork true (fn () =>
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
-            val problem = AtpWrapper.atp_problem_of_goal (get_full_types ()) i
+            val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i
               (Proof.get_goal proof_state)
             val result =
-              let val AtpWrapper.Prover_Result {success, message, ...} =
+              let val ATP_Wrapper.Prover_Result {success, message, ...} =
                 prover problem (get_timeout ())
               in (success, message) end
               handle ResHolClause.TOO_TRIVIAL

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 14 23:13:38 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 14 23:44:37 2009 +0200
@@ -6,11 +6,11 @@
 
 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 *)
@@ -99,7 +99,7 @@
 
 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
@@ -116,6 +116,7 @@
     end
   end
 
+
 (* wrapper for calling external prover *)
 
 fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
@@ -124,8 +125,8 @@
     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,
@@ -224,7 +225,7 @@
   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

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Oct 14 23:13:38 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Oct 14 23:44:37 2009 +0200
@@ -49,7 +49,7 @@
   val refresh_systems: unit -> unit
 end;
 
-structure AtpWrapper: ATP_WRAPPER =
+structure ATP_Wrapper: ATP_WRAPPER =
 struct
 
 (** generic ATP wrapper **)