src/HOL/Sledgehammer.thy

--- a/src/HOL/Sledgehammer.thy	Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Aug 28 16:58:27 2014 +0200
@@ -33,4 +33,8 @@
 ML_file "Tools/Sledgehammer/sledgehammer.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
 
+method_setup skolem = {*
+ Scan.succeed (SIMPLE_METHOD' o Sledgehammer_Proof_Methods.skolem_tac)
+*} "solve skolemization goals"
+
 end