# HG changeset patch
# User mengj
# Date 1133158513 -3600
# Node ID e15a825da2629976829cb63963c2907845c149e8
# Parent  4f0904ba19c2caf63101a2037914c38ea85d31a6
Added in four control flags for HOL and FOL translations.
Changed functions that perform HOL/FOL translations, and write ATP input to files.
Removed some functions that are no longer needed.

diff -r 4f0904ba19c2 -r e15a825da262 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Mon Nov 28 07:14:12 2005 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Mon Nov 28 07:15:13 2005 +0100
@@ -8,7 +8,14 @@
 
 val keep_atp_input = ref false;
 val debug = ref true;
-val filter_ax = ref false;
+
+val fol_keep_types = ResClause.keep_types;
+val hol_keep_types = ResHolClause.keep_types;
+
+val include_combS = ResHolClause.include_combS;
+val include_min_comb = ResHolClause.include_min_comb;
+
+
 
 (*******************************************************)
 (* set up the output paths                             *)
@@ -30,6 +37,25 @@
 	(ResAtp.helper_path "E_HOME" "additionals/u_comb_noS"
 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_noS");
 
+
+fun typed_HOL_helper1 () = 
+    ResAtp.helper_path "E_HOME" "additionals/helper1"
+    handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/helper1";
+
+
+fun untyped_HOL_helper1 () = 
+    ResAtp.helper_path "E_HOME" "additionals/u_helper1"
+    handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_helper1";
+
+
+fun HOL_helper1 () =
+    if !hol_keep_types then typed_HOL_helper1 () else untyped_HOL_helper1 ();
+
+
+fun HOL_comb () =
+    if !hol_keep_types then typed_comb() else untyped_comb();
+
+
 val claset_file = File.tmp_path (Path.basic "claset");
 val simpset_file = File.tmp_path (Path.basic "simp");
 val local_lemma_file = File.tmp_path (Path.basic "locallemmas");
@@ -60,21 +86,128 @@
 val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
 
 
-fun get_local_claR ctxt = 
-    let val cla_rules = rep_cs (Classical.get_local_claset ctxt) 
-	val safeEs = #safeEs cla_rules
-	val safeIs = #safeIs cla_rules
-	val hazEs = #hazEs cla_rules
-	val hazIs = #hazIs cla_rules
+(******************************************************************)
+(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
+(******************************************************************)
+
+datatype logic = FOL | HOL | HOLC | HOLCS;
+
+fun string_of_logic FOL = "FOL"
+  | string_of_logic HOL = "HOL"
+  | string_of_logic HOLC = "HOLC"
+  | string_of_logic HOLCS = "HOLCS";
+
+(*HOLCS will not occur here*)
+fun upgrade_lg HOLC _ = HOLC
+  | upgrade_lg HOL HOLC = HOLC
+  | upgrade_lg HOL _ = HOL
+  | upgrade_lg FOL lg = lg; 
+
+(* check types *)
+fun has_bool (Type("bool",_)) = true
+  | has_bool (Type(_, Ts)) = exists has_bool Ts
+  | has_bool _ = false;
+
+fun has_bool_arg tp = 
+    let val (targs,tr) = strip_type tp
     in
-	map ResAxioms.pairname (safeEs @ safeIs @ hazEs @ hazIs)
+	exists has_bool targs
     end;
 
+fun is_fn_tp (Type("fun",_)) = true
+  | is_fn_tp _ = false;
 
-fun get_local_simpR ctxt = 
-    let val simpset_rules = #rules(fst (rep_ss (Simplifier.get_local_simpset ctxt)))
+
+exception FN_LG of term;
+
+fun fn_lg (t as Const(f,tp)) (lg,seen) = 
+    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
+  | fn_lg (t as Free(f,tp)) (lg,seen) = 
+    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
+  | fn_lg (t as Var(f,tp)) (lg,seen) =
+    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
+    else (lg,t ins seen)
+  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
+  | fn_lg f _ = raise FN_LG(f); 
+
+
+fun term_lg [] (lg,seen) = (lg,seen)
+  | term_lg (tm::tms) (FOL,seen) =
+    let val (f,args) = strip_comb tm
+	val (lg',seen') = if f mem seen then (FOL,seen) 
+			  else fn_lg f (FOL,seen)
+
+	 in
+	     term_lg (args@tms) (lg',seen')
+    end
+  | term_lg _ (lg,seen) = (lg,seen)
+
+exception PRED_LG of term;
+
+fun pred_lg (t as Const(P,tp)) (lg,seen)= 
+    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
+  | pred_lg (t as Free(P,tp)) (lg,seen) =
+    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
+  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
+  | pred_lg P _ = raise PRED_LG(P);
+
+
+fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
+  | lit_lg P (lg,seen) =
+    let val (pred,args) = strip_comb P
+	val (lg',seen') = if pred mem seen then (lg,seen) 
+			  else pred_lg pred (lg,seen)
     in
-	map (fn r => (#name r, #thm r)) (Net.entries simpset_rules) end;
+	term_lg args (lg',seen')
+    end;
+
+fun lits_lg [] (lg,seen) = (lg,seen)
+  | lits_lg (lit::lits) (FOL,seen) =
+    lits_lg lits (lit_lg lit (FOL,seen))
+  | lits_lg lits (lg,seen) = (lg,seen);
+
+
+fun logic_of_clause tm (lg,seen) =
+    let val tm' = HOLogic.dest_Trueprop tm
+	val disjs = HOLogic.dest_disj tm'
+    in
+	lits_lg disjs (lg,seen)
+    end;
+
+fun lits_lg [] (lg,seen) = (lg,seen)
+  | lits_lg (lit::lits) (FOL,seen) =
+    lits_lg lits (lit_lg lit (FOL,seen))
+  | lits_lg lits (lg,seen) = (lg,seen);
+
+
+fun logic_of_clause tm (lg,seen) =
+    let val tm' = HOLogic.dest_Trueprop tm
+	val disjs = HOLogic.dest_disj tm'
+    in
+	lits_lg disjs (lg,seen)
+    end;
+
+fun logic_of_clauses [] (lg,seen) = (lg,seen)
+  | logic_of_clauses (cls::clss) (FOL,seen) =
+    logic_of_clauses clss (logic_of_clause cls (FOL,seen))
+  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
+
+fun logic_of_nclauses [] (lg,seen) = (lg,seen)
+  | logic_of_nclauses (cls::clss) (FOL,seen) =
+    logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
+  | logic_of_nclauses clss (lg,seen) = (lg,seen);
+
+
+
+fun problem_logic (conj_cls,hyp_cls,userR,claR,simpR) =
+    let val (lg1,seen1) = logic_of_clauses conj_cls (FOL,[])
+	val (lg2,seen2) = logic_of_clauses hyp_cls (lg1,seen1)
+	val (lg3,seen3) = logic_of_nclauses userR (lg2,seen2)
+	val (lg4,seen4) = logic_of_nclauses claR (lg3,seen3)
+	val (lg5,seen5) = logic_of_nclauses simpR (lg4,seen4)
+    in
+	lg5
+    end;
 
 
 
@@ -83,113 +216,138 @@
 (* TPTP                                                        *)
 (***************************************************************)
 
+(**** CNF rules and hypothesis ****)
+fun cnf_rules_tms ctxt ths (include_claset,include_simpset) =
+    let val local_claR = if include_claset then ResAxioms.claset_rules_of_ctxt ctxt else []
+	val (local_claR_cls,err1) = ResAxioms.cnf_rules2 local_claR []
+	val local_simpR = if include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt else []
+	val (local_simpR_cls,err2) = ResAxioms.cnf_rules2 local_simpR []
+	val (user_ths_cls,err3) = ResAxioms.cnf_rules2 (map ResAxioms.pairname ths) []
+	val errs = err3 @ err2 @ err1
+    in
+	(user_ths_cls,local_simpR_cls,local_claR_cls,errs)
+    end;
 
+fun cnf_hyps_thms ctxt = 
+    let val ths = ProofContext.prems_of ctxt
+	val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux ths)
+    in
+	prems
+    end;
+
+(**** clausification ****)
+fun cls_axiom_fol _ _ [] = []
+  | cls_axiom_fol name i (tm::tms) =
+   (ResClause.make_axiom_clause tm (name,i)) :: (cls_axiom_fol name (i+1) tms);
+
+fun cls_axiom_hol  _ _ [] = []
+  | cls_axiom_hol name i (tm::tms) =
+   (ResHolClause.make_axiom_clause tm (name,i)) :: (cls_axiom_hol name (i+1) tms);
 
 
-(***************** TPTP format *********************************)
+fun filtered_tptp_axiom_fol name clss =
+    (fst(ListPair.unzip (map ResClause.clause2tptp (filter (fn c => not (ResClause.isTaut c)) (cls_axiom_fol name 0 clss)))),[])
+    handle _ => ([],[name]);
 
-(* convert each (sub)goal clause (Thm.thm) into one or more TPTP clauses.  The additional TPTP clauses are tfree_lits.  Write the output TPTP clauses to a problem file *)
+fun filtered_tptp_axiom_hol name clss =
+    (fst(ListPair.unzip (map ResHolClause.clause2tptp (filter (fn c => not (ResHolClause.isTaut c)) (cls_axiom_hol name 0 clss)))),[])
+    handle _ => ([],[name]);
 
-fun mk_conjectures is_fol terms =
-    if is_fol then
-	ListPair.unzip (map ResClause.clause2tptp (ResClause.make_conjecture_clauses terms))
-    else
-	ListPair.unzip (map ResHolClause.clause2tptp (ResHolClause.make_conjecture_clauses terms));
+fun tptp_axioms_g filt_ax_fn [] err = ([],err)
+  | tptp_axioms_g filt_ax_fn ((name,clss)::nclss) err =
+    let val (nclss1,err1) = tptp_axioms_g filt_ax_fn nclss err
+	val (clsstrs,err_name_list) = filt_ax_fn name clss
+    in
+	case clsstrs of [] => (nclss1,err_name_list @ err1) 
+		      | _ => (clsstrs::nclss1,err1)
+    end;
+		
+fun tptp_axioms_fol rules = tptp_axioms_g filtered_tptp_axiom_fol rules [];
+
+fun tptp_axioms_hol rules = tptp_axioms_g filtered_tptp_axiom_hol rules [];
+
+
+fun atp_axioms_g tptp_ax_fn rules file =
+    let val out = TextIO.openOut file
+	val (clss,errs) = tptp_ax_fn rules
+	val clss' = ResClause.union_all clss
+    in
+	ResAtp.writeln_strs out clss';
+	TextIO.closeOut out;
+	([file],errs)
+    end;
 
 
-fun tptp_form_g is_fol thms n tfrees =
-    let val terms = map prop_of thms
-	val (tptp_clss,tfree_litss) = mk_conjectures is_fol terms
+fun atp_axioms_fol rules file = atp_axioms_g tptp_axioms_fol rules file;
+
+fun atp_axioms_hol rules file = atp_axioms_g tptp_axioms_hol rules file;
+
+
+fun filtered_tptp_conjectures_fol terms =
+    let val clss = ResClause.make_conjecture_clauses terms
+	val clss' = filter (fn c => not (ResClause.isTaut c)) clss
+    in
+	ListPair.unzip (map ResClause.clause2tptp clss')
+    end;
+
+fun filtered_tptp_conjectures_hol terms =
+    let val clss = ResHolClause.make_conjecture_clauses terms
+	val clss' = filter (fn c => not (ResHolClause.isTaut c)) clss
+    in
+	ListPair.unzip (map ResHolClause.clause2tptp clss')
+    end;
+
+fun atp_conjectures_h_g filt_conj_fn hyp_cls =
+    let val (tptp_h_clss,tfree_litss) = filt_conj_fn hyp_cls
+	val tfree_lits = ResClause.union_all tfree_litss
+	val tfree_clss = map ResClause.tfree_clause tfree_lits 
+	val hypsfile = File.platform_path hyps_file
+        val out = TextIO.openOut(hypsfile)
+    in
+        ResAtp.writeln_strs out (tfree_clss @ tptp_h_clss);
+        TextIO.closeOut out; warning hypsfile;
+        ([hypsfile],tfree_lits)
+    end;
+
+fun atp_conjectures_h_fol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_fol hyp_cls;
+
+fun atp_conjectures_h_hol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_hol hyp_cls;
+
+fun atp_conjectures_c_g filt_conj_fn conj_cls n tfrees =
+    let val (tptp_c_clss,tfree_litss) = filt_conj_fn conj_cls
 	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
 	val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
 	val out = TextIO.openOut(probfile)		 	
     in
-	ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
+	ResAtp.writeln_strs out (tfree_clss @ tptp_c_clss);
 	TextIO.closeOut out;
-	warning probfile; (* show the location for debugging *)
-	probfile (* return the location *)
-	
+	warning probfile; 
+	probfile 
     end;
 
-
-val tptp_form = tptp_form_g true;
-val tptp_formH = tptp_form_g false;
+fun atp_conjectures_c_fol conj_cls n tfrees = atp_conjectures_c_g filtered_tptp_conjectures_fol conj_cls n tfrees;
 
-fun tptp_hyps_g _ [] = ([], [])
-  | tptp_hyps_g is_fol thms =
-    let val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux thms)
-	val prems' = map prop_of prems
-	val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'
-	val tfree_lits = ResClause.union_all tfree_litss
-	val tfree_clss = map ResClause.tfree_clause tfree_lits 
-        val hypsfile = File.platform_path hyps_file
-        val out = TextIO.openOut(hypsfile)
-    in
-        ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
-        TextIO.closeOut out; warning hypsfile;
-        ([hypsfile],tfree_lits)
-    end;
- 
-
-val tptp_hyps = tptp_hyps_g true;
-val tptp_hypsH = tptp_hyps_g false;
-
-fun mk_axioms is_fol rules =
-    if is_fol then 
-	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
-	     val (clss',names) = ListPair.unzip clss
-	     val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
-	 in tptpclss end)
-    else
-	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairsH rules)
-	     val (clss',names) = ListPair.unzip clss
-	     val (tptpclss,_) = ListPair.unzip(map ResHolClause.clause2tptp clss')
-	 in tptpclss end)
+fun atp_conjectures_c_hol conj_cls n tfrees = atp_conjectures_c_g filtered_tptp_conjectures_hol conj_cls n tfrees;
 
 
-
-fun write_rules_g is_fol [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
-  | write_rules_g is_fol rules file =
-    let val out = TextIO.openOut(file)
-	val tptpclss = mk_axioms is_fol rules
+fun atp_conjectures_g atp_conj_h_fn atp_conj_c_fn [] conj_cls n =
+    let val probfile = atp_conj_c_fn conj_cls n []
     in
-	ResAtp.writeln_strs out tptpclss;
-	TextIO.closeOut out; warning file;
-	[file]
+	[probfile]
+    end
+  | atp_conjectures_g atp_conj_h_fn atp_conj_c_fn hyp_cls conj_cls n =
+    let val (hypsfile,tfree_lits) = atp_conj_h_fn hyp_cls
+	val probfile = atp_conj_c_fn conj_cls n tfree_lits
+    in
+	(probfile::hypsfile)
     end;
 
+fun atp_conjectures_fol hyp_cls conj_cls n = atp_conjectures_g atp_conjectures_h_fol atp_conjectures_c_fol hyp_cls conj_cls n;
 
-val write_rules = write_rules_g true;
-val write_rulesH = write_rules_g false;
-
+fun atp_conjectures_hol hyp_cls conj_cls n = atp_conjectures_g atp_conjectures_h_hol atp_conjectures_c_hol hyp_cls conj_cls n;
 
 
-(* TPTP Isabelle theorems *)
-fun tptp_cnf_rules_g write_rules ths (clasetR,simpsetR) =
-    let val simpfile = File.platform_path simpset_file
-	val clafile =  File.platform_path claset_file
-	val local_lemfile = File.platform_path local_lemma_file
-    in
-	(write_rules clasetR clafile) @ (write_rules simpsetR simpfile) @ (write_rules ths local_lemfile)
-    end;
-
-val tptp_cnf_rules = tptp_cnf_rules_g write_rules;
-val tptp_cnf_rulesH = tptp_cnf_rules_g write_rulesH;
-
-
-fun tptp_cnf_clasimp_g tptp_cnf_rules ths ctxt (include_claset,include_simpset) =
-    let val local_claR = if include_claset then get_local_claR ctxt else []
-	val local_simpR = if include_simpset then get_local_simpR ctxt else []
-	val ths_names = map ResAxioms.pairname ths
-    in
-	tptp_cnf_rules ths_names (local_claR,local_simpR)
-    end;
-
-
-val tptp_cnf_clasimp  = tptp_cnf_clasimp_g tptp_cnf_rules;
-val tptp_cnf_clasimpH = tptp_cnf_clasimp_g tptp_cnf_rulesH;
-
-
+(**** types and sorts ****)
 fun tptp_types_sorts thy = 
     let val classrel_clauses = ResClause.classrel_clauses_thy thy
 	val arity_clauses = ResClause.arity_clause_thy thy
@@ -210,45 +368,80 @@
     end;
 
 
+(******* write to files ******)
 
-(*FIXME: a function that does not perform any filtering now *)
-fun find_relevant_ax tptp_cnf_clasimp ths ctxt = tptp_cnf_clasimp ths ctxt (true,true);
+datatype mode = Auto | Fol | Hol;
+
+fun write_out_g logic atp_ax_fn atp_conj_fn (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
+    let val (files1,err1) = if (null claR) then ([],[]) else (atp_ax_fn claR (File.platform_path claset_file))
+	val (files2,err2) = if (null simpR) then ([],[]) else (atp_ax_fn simpR (File.platform_path simpset_file))
+	val (files3,err3) = if (null userR) then ([],[]) else (atp_ax_fn userR (File.platform_path local_lemma_file))
+	val files4 = atp_conj_fn hyp_cls conj_cls n
+	val errs = err1 @ err2 @ err3 @ err
+	val logic' = if !include_combS then HOLCS 
+		     else 
+			 if !include_min_comb then HOLC else logic
+	val _ = warning ("Problems are " ^ (string_of_logic logic'))
+	val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
+	val helpers = case logic' of FOL => []
+				   | HOL => [HOL_helper1 ()]
+				   | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
+    in
+	include_min_comb:=false; (*reset to false*)
+	include_combS:=false; (*reset to false*)
+	(helpers,files4 @ files1 @ files2 @ files3)
+    end;
+
+fun write_out_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err) = write_out_g FOL atp_axioms_fol atp_conjectures_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err);
+
+fun write_out_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err) = write_out_g HOL atp_axioms_hol atp_conjectures_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err);
+
+fun write_out_fol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =  
+    let val ts_file = if (!fol_keep_types) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
+	val (helpers,files) = write_out_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err) 
+    in
+	(helpers,files@ts_file)
+    end;
+
+fun write_out_hol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =  
+    let val ts_file = if (!hol_keep_types) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
+	val (helpers,files) = write_out_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err)
+    in
+	(helpers,files@ts_file)
+    end;
+
+
+fun prep_atp_input mode ctxt conjectures user_thms n =
+    let val conj_cls = map prop_of (make_clauses conjectures) 
+	val (userR,simpR,claR,errs) = cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset) 
+	val hyp_cls = map prop_of (cnf_hyps_thms ctxt) 
+	val logic = case mode of Auto => problem_logic (conj_cls,hyp_cls,userR,claR,simpR)
+			       | Fol => FOL
+			       | Hol => HOL
+    in
+	case logic of FOL => write_out_fol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
+		    | _ => write_out_hol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
+			   
+    end;
 
 
 (***************************************************************)
 (* setup ATPs as Isabelle methods                              *)
 (***************************************************************)
-fun atp_meth_g helper_file tptp_hyps tptp_cnf_clasimp tac ths ctxt = 
-    let val rules = if !filter_ax then find_relevant_ax tptp_cnf_clasimp ths ctxt 
-		    else tptp_cnf_clasimp ths ctxt (!include_claset, !include_simpset) 
-	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
-	val thy = ProofContext.theory_of ctxt
-	val tsfile = tptp_types_sorts thy
-	val files = (helper_file,hyps @ rules @ tsfile)
+
+
+fun atp_meth' tac ths ctxt = 
+    Method.SIMPLE_METHOD' HEADGOAL
+    (tac ctxt ths);
+
+fun atp_meth tac ths ctxt = 
+    let val _ = ResClause.init (ProofContext.theory_of ctxt)
     in
-	Method.SIMPLE_METHOD' HEADGOAL
-	(tac ctxt files tfrees)
-    end;
-fun atp_meth_f tac ths ctxt = atp_meth_g [] tptp_hyps tptp_cnf_clasimp tac ths ctxt;
-fun atp_meth_h tac ths ctxt = 
-    let val helper = if !ResHolClause.keep_types then [typed_comb ()] else [untyped_comb ()]
-    in
-	atp_meth_g helper tptp_hypsH tptp_cnf_clasimpH tac ths ctxt
+	atp_meth' tac ths ctxt
     end;
 
 
-fun atp_meth_G atp_meth tac ths ctxt =
-    let val _  = ResClause.init (ProofContext.theory_of ctxt)
-    in
-	atp_meth tac ths ctxt
-    end;
-fun atp_meth_H tac ths ctxt = atp_meth_G atp_meth_h tac ths ctxt;
-fun atp_meth_F tac ths ctxt = atp_meth_G atp_meth_f tac ths ctxt;
-
-
-fun atp_method_H tac = Method.thms_ctxt_args (atp_meth_H tac);
-fun atp_method_F tac = Method.thms_ctxt_args (atp_meth_F tac);
-
+fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
 
 
 (*************Remove tmp files********************************)