src/HOL/Tools/res_atp.ML
changeset 20289 ba7a7c56bed5
parent 20246 fdfe7399e057
child 20372 e42674e0486e
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 02 22:26:40 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 02 22:26:41 2006 +0200
     1.3 @@ -26,8 +26,8 @@
     1.4    val vampireLimit: unit -> int
     1.5    val eproverLimit: unit -> int
     1.6    val spassLimit: unit -> int
     1.7 -  val atp_method: (ProofContext.context -> thm list -> int -> Tactical.tactic) ->
     1.8 -		  Method.src -> ProofContext.context -> Method.method
     1.9 +  val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    1.10 +    Method.src -> Proof.context -> Proof.method
    1.11    val cond_rm_tmp: string -> unit
    1.12    val keep_atp_input: bool ref
    1.13    val fol_keep_types: bool ref