removed the functions for getting HOL helper paths.
authormengj
Fri Apr 28 05:58:53 2006 +0200 (2006-04-28 ago)
changeset 19490bf7f8347174a
parent 19489 4441b637871b
child 19491 cd6c71c57f53
removed the functions for getting HOL helper paths.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Apr 27 17:48:41 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Apr 28 05:58:53 2006 +0200
     1.3 @@ -133,70 +133,6 @@
     1.4  val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
     1.5  val rm_atpset = (fn () => include_atpset:=false);
     1.6  
     1.7 -(*** paths for HOL helper files ***)
     1.8 -fun full_typed_comb_inclS () =
     1.9 -    helper_path "E_HOME" "additionals/full_comb_inclS"
    1.10 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS";
    1.11 -
    1.12 -fun full_typed_comb_noS () =
    1.13 -    helper_path "E_HOME" "additionals/full_comb_noS"
    1.14 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS";
    1.15 -									      
    1.16 -fun partial_typed_comb_inclS () =
    1.17 -    helper_path "E_HOME" "additionals/par_comb_inclS"
    1.18 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS";
    1.19 -
    1.20 -fun partial_typed_comb_noS () =
    1.21 -    helper_path "E_HOME" "additionals/par_comb_noS"
    1.22 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS";
    1.23 -
    1.24 -fun const_typed_comb_inclS () =
    1.25 -    helper_path "E_HOME" "additionals/const_comb_inclS"
    1.26 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS";
    1.27 -
    1.28 -fun const_typed_comb_noS () =
    1.29 -    helper_path "E_HOME" "additionals/const_comb_noS"
    1.30 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS";
    1.31 -
    1.32 -fun untyped_comb_inclS () =
    1.33 -    helper_path "E_HOME" "additionals/u_comb_inclS"
    1.34 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS";
    1.35 -
    1.36 -fun untyped_comb_noS () =
    1.37 -    helper_path "E_HOME" "additionals/u_comb_noS"
    1.38 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS";
    1.39 -
    1.40 -fun full_typed_HOL_helper1 () =
    1.41 -    helper_path "E_HOME" "additionals/full_helper1"
    1.42 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1";
    1.43 -
    1.44 -fun partial_typed_HOL_helper1 () = 
    1.45 -    helper_path "E_HOME" "additionals/par_helper1"
    1.46 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1";
    1.47 -
    1.48 -fun const_typed_HOL_helper1 () = 
    1.49 -    helper_path "E_HOME" "additionals/const_helper1"
    1.50 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1";
    1.51 -
    1.52 -fun untyped_HOL_helper1 () = 
    1.53 -    helper_path "E_HOME" "additionals/u_helper1"
    1.54 -    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1";
    1.55 -
    1.56 -fun get_full_typed_helpers () =
    1.57 -    (full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ());
    1.58 -
    1.59 -fun get_partial_typed_helpers () =
    1.60 -    (partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ());
    1.61 -
    1.62 -fun get_const_typed_helpers () =
    1.63 -    (const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ());
    1.64 -
    1.65 -fun get_untyped_helpers () =
    1.66 -    (untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ());
    1.67 -
    1.68 -fun get_all_helpers () =
    1.69 -    (get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ());
    1.70 -
    1.71  
    1.72  (**** relevance filter ****)
    1.73  val run_relevance_filter = ref true;
    1.74 @@ -347,8 +283,7 @@
    1.75  fun tptp_writer logic goals filename (axioms,classrels,arities) =
    1.76      if is_fol_logic logic 
    1.77      then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
    1.78 -    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) 
    1.79 -	   (get_all_helpers());
    1.80 +    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities);
    1.81  
    1.82  (*2006-04-07: not working: goals has type thm list (not term list as above) and
    1.83    axioms has type ResClause.clause list (not (thm * (string * int)) list as above)*)