# HG changeset patch
# User blanchet
# Date 1277278806 -7200
# Node ID 26afa11a1fb20b5e73b95f3d76b5337df14557c5
# Parent  6d9923e8d2083df2ddf0cef855ce07c3b631cea3
killed legacy "neg_clausify" and "clausify"

diff -r 6d9923e8d208 -r 26afa11a1fb2 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Jun 22 23:54:16 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Wed Jun 23 09:40:06 2010 +0200
@@ -110,7 +110,6 @@
 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 6d9923e8d208 -r 26afa11a1fb2 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 23:54:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Jun 23 09:40:06 2010 +0200
@@ -22,11 +22,9 @@
   val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
   val saturate_skolem_cache: theory -> theory option
   val auto_saturate_skolem_cache: bool Unsynchronized.ref
-    (* for emergency use where the Skolem cache causes problems *)
   val neg_clausify: thm -> thm list
   val neg_conjecture_clauses:
     Proof.context -> thm -> int -> thm list list * (string * typ) list
-  val neg_clausify_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end;
 
@@ -522,6 +520,7 @@
 
 end;
 
+(* For emergency use where the Skolem cache causes problems. *)
 val auto_saturate_skolem_cache = Unsynchronized.ref true
 
 fun conditionally_saturate_skolem_cache thy =
@@ -547,20 +546,6 @@
       Subgoal.focus (Variable.set_body false ctxt) n st
   in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
 
-(*Conversion of a subgoal to conjecture clauses. Each clause has
-  leading !!-bound universal variables, to express generality. *)
-fun neg_clausify_tac ctxt =
-  neg_skolemize_tac ctxt THEN'
-  SUBGOAL (fn (prop, i) =>
-    let val ts = Logic.strip_assums_hyp prop in
-      EVERY'
-       [Subgoal.FOCUS
-         (fn {prems, ...} =>
-           (Method.insert_tac
-             (map forall_intr_vars (maps neg_clausify prems)) i)) ctxt,
-        REPEAT_DETERM_N (length ts) o etac thin_rl] i
-     end);
-
 
 (** setup **)
 
diff -r 6d9923e8d208 -r 26afa11a1fb2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 22 23:54:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 23 09:40:06 2010 +0200
@@ -12,7 +12,6 @@
   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 =
@@ -25,31 +24,6 @@
 open ATP_Systems
 open Sledgehammer_Fact_Minimizer
 
-(** Proof method used in Isar proofs **)
-
-val neg_clausify_setup =
-  Method.setup @{binding neg_clausify}
-               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)
-                o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \
-                                   \rerun Sledgehammer to obtain a direct \
-                                   \proof"))
-               "conversion of goal to negated conjecture clauses (legacy)"
-
-(** Attribute for converting a theorem into clauses **)
-
-val parse_clausify_attribute : attribute context_parser =
-  Scan.lift Parse.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))
-
-val clausify_setup =
-  Attrib.setup @{binding clausify}
-               (parse_clausify_attribute
-                o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
-               "conversion of theorem to clauses"
-
 (** Sledgehammer commands **)
 
 fun add_to_relevance_override ns : relevance_override =
@@ -357,8 +331,4 @@
       "set and display the default parameters for Sledgehammer" Keyword.thy_decl
       parse_sledgehammer_params_command
 
-val setup =
-  neg_clausify_setup
-  #> clausify_setup
-
 end;