src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 32936 9491bec20595
parent 32865 f8d1e16ec758
child 32937 34f66c9dd8a2
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:13:38 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:44:37 2009 +0200
     1.3 @@ -21,13 +21,13 @@
     1.4    val kill: unit -> unit
     1.5    val info: unit -> unit
     1.6    val messages: int option -> unit
     1.7 -  val add_prover: string * AtpWrapper.prover -> theory -> theory
     1.8 +  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
     1.9    val print_provers: theory -> unit
    1.10 -  val get_prover: string -> theory -> AtpWrapper.prover option
    1.11 +  val get_prover: string -> theory -> ATP_Wrapper.prover option
    1.12    val sledgehammer: string list -> Proof.state -> unit
    1.13  end;
    1.14  
    1.15 -structure AtpManager: ATP_MANAGER =
    1.16 +structure ATP_Manager: ATP_MANAGER =
    1.17  struct
    1.18  
    1.19  (** preferences **)
    1.20 @@ -302,7 +302,7 @@
    1.21  
    1.22  structure Provers = TheoryDataFun
    1.23  (
    1.24 -  type T = (AtpWrapper.prover * stamp) Symtab.table
    1.25 +  type T = (ATP_Wrapper.prover * stamp) Symtab.table
    1.26    val empty = Symtab.empty
    1.27    val copy = I
    1.28    val extend = I
    1.29 @@ -337,10 +337,10 @@
    1.30          val _ = SimpleThread.fork true (fn () =>
    1.31            let
    1.32              val _ = register birthtime deadtime (Thread.self (), desc)
    1.33 -            val problem = AtpWrapper.atp_problem_of_goal (get_full_types ()) i
    1.34 +            val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i
    1.35                (Proof.get_goal proof_state)
    1.36              val result =
    1.37 -              let val AtpWrapper.Prover_Result {success, message, ...} =
    1.38 +              let val ATP_Wrapper.Prover_Result {success, message, ...} =
    1.39                  prover problem (get_timeout ())
    1.40                in (success, message) end
    1.41                handle ResHolClause.TOO_TRIVIAL