--- a/src/HOL/Tools/res_atp.ML Fri Apr 27 18:50:27 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Apr 30 13:22:15 2007 +0200
@@ -31,11 +31,6 @@
val atp_method: (Proof.context -> thm list -> int -> tactic) ->
Method.src -> Proof.context -> Proof.method
val cond_rm_tmp: string -> unit
- val hol_full_types: unit -> unit
- val hol_partial_types: unit -> unit
- val hol_const_types_only: unit -> unit
- val hol_no_types: unit -> unit
- val hol_typ_level: unit -> ResHolClause.type_level
val include_all: bool ref
val run_relevance_filter: bool ref
val run_blacklist_filter: bool ref
@@ -134,17 +129,6 @@
fun eproverLimit () = !eprover_time;
fun spassLimit () = !spass_time;
-val hol_full_types = ResHolClause.full_types;
-val hol_partial_types = ResHolClause.partial_types;
-val hol_const_types_only = ResHolClause.const_types_only;
-val hol_no_types = ResHolClause.no_types;
-fun hol_typ_level () = ResHolClause.find_typ_level ();
-fun is_typed_hol () =
- let val tp_level = hol_typ_level()
- in
- not (tp_level = ResHolClause.T_NONE)
- end;
-
fun atp_input_file () =
let val file = !problem_name
in