diff -r 91d893799212 -r e170cee91c66 src/HOL/Tools/res_atp_methods.ML
--- 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)