# HG changeset patch
# User blanchet
# Date 1272199236 -7200
# Node ID 1a48d18449d8e72140d90d0a0144cf658d418fde
# Parent  be73a2b2443b18c68d713734c0f04518297522d7
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"

diff -r be73a2b2443b -r 1a48d18449d8 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Sun Apr 25 11:38:46 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Sun Apr 25 14:40:36 2010 +0200
@@ -105,6 +105,7 @@
 setup ATP_Systems.setup
 use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
 use "Tools/Sledgehammer/sledgehammer_isar.ML"
+setup Sledgehammer_Isar.setup
 
 
 subsection {* The MESON prover *}
diff -r be73a2b2443b -r 1a48d18449d8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 25 11:38:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 25 14:40:36 2010 +0200
@@ -20,6 +20,7 @@
   val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
   val suppress_endtheory: bool Unsynchronized.ref
     (*for emergency use where endtheory causes problems*)
+  val neg_clausify_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end;
 
@@ -484,26 +485,10 @@
         REPEAT_DETERM_N (length ts) o etac thin_rl] i
      end);
 
-val neg_clausify_setup =
-  Method.setup @{binding neg_clausify} (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
-  "conversion of goal to conjecture clauses";
-
-
-(** Attribute for converting a theorem into clauses **)
-
-val clausify_setup =
-  Attrib.setup @{binding clausify}
-    (Scan.lift OuterParse.nat >>
-      (fn i => Thm.rule_attribute (fn context => fn th =>
-          Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
-  "conversion of theorem to clauses";
-
 
 (** setup **)
 
 val setup =
-  neg_clausify_setup #>
-  clausify_setup #>
   perhaps saturate_skolem_cache #>
   Theory.at_end clause_cache_endtheory;
 
diff -r be73a2b2443b -r 1a48d18449d8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Apr 25 11:38:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Apr 25 14:40:36 2010 +0200
@@ -12,18 +12,42 @@
   val timeout: int Unsynchronized.ref
   val full_types: bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
+  val setup: theory -> theory
 end;
 
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
 open Sledgehammer_Util
+open Sledgehammer_Fact_Preprocessor
 open ATP_Manager
 open ATP_Systems
 open Sledgehammer_Fact_Minimizer
 
 structure K = OuterKeyword and P = OuterParse
 
+(** Proof method used in Isar proofs **)
+
+val neg_clausify_setup =
+  Method.setup @{binding neg_clausify}
+               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
+               "conversion of goal to negated conjecture clauses"
+
+val parse_clausify_attribute =
+  Scan.lift OuterParse.nat
+  >> (fn i => Thm.rule_attribute (fn context => fn th =>
+                  let val thy = Context.theory_of context in
+                    Meson.make_meta_clause (nth (cnf_axiom thy th) i)
+                  end))
+
+(** Attribute for converting a theorem into clauses **)
+
+val clausify_setup =
+  Attrib.setup @{binding clausify} parse_clausify_attribute
+               "conversion of theorem to clauses"
+
+(** Sledgehammer commands **)
+
 fun add_to_relevance_override ns : relevance_override =
   {add = ns, del = [], only = false}
 fun del_from_relevance_override ns : relevance_override =
@@ -323,11 +347,15 @@
 
 val _ =
   OuterSyntax.improper_command sledgehammerN
-    "search for first-order proof using automatic theorem provers" K.diag
-    parse_sledgehammer_command
+      "search for first-order proof using automatic theorem provers" K.diag
+      parse_sledgehammer_command
 val _ =
   OuterSyntax.command sledgehammer_paramsN
-    "set and display the default parameters for Sledgehammer" K.thy_decl
-    parse_sledgehammer_params_command
+      "set and display the default parameters for Sledgehammer" K.thy_decl
+      parse_sledgehammer_params_command
+
+val setup =
+  neg_clausify_setup
+  #> clausify_setup
 
 end;