--- a/src/HOL/Tools/res_atp_setup.ML Fri Oct 28 17:27:04 2005 +0200
+++ b/src/HOL/Tools/res_atp_setup.ML Fri Oct 28 17:27:49 2005 +0200
@@ -251,10 +251,9 @@
else HEADGOAL (tac ctxt files tfrees))
end;
-val atp_meth_f = atp_meth_g tptp_hyps tptp_cnf_clasimp;
+fun atp_meth_f tac = atp_meth_g tptp_hyps tptp_cnf_clasimp tac;
-val atp_meth_h = atp_meth_g tptp_hypsH tptp_cnf_clasimpH;
-
+fun atp_meth_h tac = atp_meth_g tptp_hypsH tptp_cnf_clasimpH tac;
fun atp_meth_G atp_meth tac prems ctxt =
let val _ = ResClause.init (ProofContext.theory_of ctxt)
@@ -264,9 +263,9 @@
end;
-val atp_meth_H = atp_meth_G atp_meth_h;
+fun atp_meth_H tac = atp_meth_G atp_meth_h tac;
-val atp_meth_F = atp_meth_G atp_meth_f;
+fun atp_meth_F tac = atp_meth_G atp_meth_f tac;
val atp_method_H = Method.bang_sectioned_args rules_modifiers o atp_meth_H;