--- a/src/HOL/Tools/res_atp_methods.ML Thu Aug 16 21:52:08 2007 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML Fri Aug 17 00:03:50 2007 +0200
@@ -9,7 +9,7 @@
(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
- (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac,
+ (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac,
METAHYPS(fn negs =>
HEADGOAL(Tactic.rtac
(res_atp_oracle (ProofContext.theory_of ctxt)