# HG changeset patch
# User mengj
# Date 1146196733 -7200
# Node ID bf7f8347174a2dd9b0d5d9b848e60ad87c9de125
# Parent  4441b637871ba1f671eb8315b2667a66c954988d
removed the functions for getting HOL helper paths.

diff -r 4441b637871b -r bf7f8347174a src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Apr 27 17:48:41 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Apr 28 05:58:53 2006 +0200
@@ -133,70 +133,6 @@
 val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
 val rm_atpset = (fn () => include_atpset:=false);
 
-(*** paths for HOL helper files ***)
-fun full_typed_comb_inclS () =
-    helper_path "E_HOME" "additionals/full_comb_inclS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS";
-
-fun full_typed_comb_noS () =
-    helper_path "E_HOME" "additionals/full_comb_noS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS";
-									      
-fun partial_typed_comb_inclS () =
-    helper_path "E_HOME" "additionals/par_comb_inclS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS";
-
-fun partial_typed_comb_noS () =
-    helper_path "E_HOME" "additionals/par_comb_noS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS";
-
-fun const_typed_comb_inclS () =
-    helper_path "E_HOME" "additionals/const_comb_inclS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS";
-
-fun const_typed_comb_noS () =
-    helper_path "E_HOME" "additionals/const_comb_noS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS";
-
-fun untyped_comb_inclS () =
-    helper_path "E_HOME" "additionals/u_comb_inclS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS";
-
-fun untyped_comb_noS () =
-    helper_path "E_HOME" "additionals/u_comb_noS"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS";
-
-fun full_typed_HOL_helper1 () =
-    helper_path "E_HOME" "additionals/full_helper1"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1";
-
-fun partial_typed_HOL_helper1 () = 
-    helper_path "E_HOME" "additionals/par_helper1"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1";
-
-fun const_typed_HOL_helper1 () = 
-    helper_path "E_HOME" "additionals/const_helper1"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1";
-
-fun untyped_HOL_helper1 () = 
-    helper_path "E_HOME" "additionals/u_helper1"
-    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1";
-
-fun get_full_typed_helpers () =
-    (full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ());
-
-fun get_partial_typed_helpers () =
-    (partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ());
-
-fun get_const_typed_helpers () =
-    (const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ());
-
-fun get_untyped_helpers () =
-    (untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ());
-
-fun get_all_helpers () =
-    (get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ());
-
 
 (**** relevance filter ****)
 val run_relevance_filter = ref true;
@@ -347,8 +283,7 @@
 fun tptp_writer logic goals filename (axioms,classrels,arities) =
     if is_fol_logic logic 
     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
-    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) 
-	   (get_all_helpers());
+    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities);
 
 (*2006-04-07: not working: goals has type thm list (not term list as above) and
   axioms has type ResClause.clause list (not (thm * (string * int)) list as above)*)