Removal of dead code
authorpaulson
Mon Apr 30 13:22:15 2007 +0200 (2007-04-30)
changeset 2282451bb2f6ecc4a
parent 22823 fa9ff469247f
child 22825 bd774e01d6d5
Removal of dead code
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Apr 27 18:50:27 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Apr 30 13:22:15 2007 +0200
     1.3 @@ -31,11 +31,6 @@
     1.4    val atp_method: (Proof.context -> thm list -> int -> tactic) ->
     1.5      Method.src -> Proof.context -> Proof.method
     1.6    val cond_rm_tmp: string -> unit
     1.7 -  val hol_full_types: unit -> unit
     1.8 -  val hol_partial_types: unit -> unit
     1.9 -  val hol_const_types_only: unit -> unit
    1.10 -  val hol_no_types: unit -> unit
    1.11 -  val hol_typ_level: unit -> ResHolClause.type_level
    1.12    val include_all: bool ref
    1.13    val run_relevance_filter: bool ref
    1.14    val run_blacklist_filter: bool ref
    1.15 @@ -134,17 +129,6 @@
    1.16  fun eproverLimit () = !eprover_time;
    1.17  fun spassLimit () = !spass_time;
    1.18  
    1.19 -val hol_full_types = ResHolClause.full_types;
    1.20 -val hol_partial_types = ResHolClause.partial_types;
    1.21 -val hol_const_types_only = ResHolClause.const_types_only;
    1.22 -val hol_no_types = ResHolClause.no_types;
    1.23 -fun hol_typ_level () = ResHolClause.find_typ_level ();
    1.24 -fun is_typed_hol () =
    1.25 -    let val tp_level = hol_typ_level()
    1.26 -    in
    1.27 -        not (tp_level = ResHolClause.T_NONE)
    1.28 -    end;
    1.29 -
    1.30  fun atp_input_file () =
    1.31      let val file = !problem_name
    1.32      in