# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID 87a8cc594bf678e87d770b3e0d458c34c2501f86
# Parent  1cd45fec98e2a9099d9f8552cc1813af1062da00
moved skolem method

diff -r 1cd45fec98e2 -r 87a8cc594bf6 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Aug 28 16:58:27 2014 +0200
@@ -110,6 +110,20 @@
     by (induct n) auto
 qed
 
+
+subsection {* A skolemization tactic and proof method *}
+
+ML {*
+fun skolem_tac ctxt =
+  Atomize_Elim.atomize_elim_tac ctxt THEN'
+  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt));
+*}
+
+method_setup skolem = {*
+ Scan.succeed (SIMPLE_METHOD' o skolem_tac)
+*} "solve skolemization goals"
+
+
 subsection {*Function Inverse*}
 
 lemma inv_def: "inv f = (%y. SOME x. f x = y)"
@@ -918,4 +932,3 @@
 ML_file "Tools/choice_specification.ML"
 
 end
-
diff -r 1cd45fec98e2 -r 87a8cc594bf6 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Aug 28 16:58:27 2014 +0200
@@ -33,8 +33,4 @@
 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
diff -r 1cd45fec98e2 -r 87a8cc594bf6 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -32,7 +32,6 @@
   type one_line_params =
     ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
-  val skolem_tac : Proof.context -> int -> tactic
   val is_proof_method_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
@@ -49,10 +48,6 @@
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 
-fun skolem_tac ctxt =
-  TRY o Atomize_Elim.atomize_elim_tac ctxt THEN'
-  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice}) THEN ALLGOALS (blast_tac ctxt))
-
 datatype proof_method =
   Metis_Method of string option * string option |
   Meson_Method |