1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 22 23:54:16 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 23 09:40:06 2010 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    val timeout: int Unsynchronized.ref
     1.5    val full_types: bool Unsynchronized.ref
     1.6    val default_params : theory -> (string * string) list -> params
     1.7 -  val setup: theory -> theory
     1.8  end;
     1.9  
    1.10  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    1.11 @@ -25,31 +24,6 @@
    1.12  open ATP_Systems
    1.13  open Sledgehammer_Fact_Minimizer
    1.14  
    1.15 -(** Proof method used in Isar proofs **)
    1.16 -
    1.17 -val neg_clausify_setup =
    1.18 -  Method.setup @{binding neg_clausify}
    1.19 -               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)
    1.20 -                o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \
    1.21 -                                   \rerun Sledgehammer to obtain a direct \
    1.22 -                                   \proof"))
    1.23 -               "conversion of goal to negated conjecture clauses (legacy)"
    1.24 -
    1.25 -(** Attribute for converting a theorem into clauses **)
    1.26 -
    1.27 -val parse_clausify_attribute : attribute context_parser =
    1.28 -  Scan.lift Parse.nat
    1.29 -  >> (fn i => Thm.rule_attribute (fn context => fn th =>
    1.30 -                  let val thy = Context.theory_of context in
    1.31 -                    Meson.make_meta_clause (nth (cnf_axiom thy th) i)
    1.32 -                  end))
    1.33 -
    1.34 -val clausify_setup =
    1.35 -  Attrib.setup @{binding clausify}
    1.36 -               (parse_clausify_attribute
    1.37 -                o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
    1.38 -               "conversion of theorem to clauses"
    1.39 -
    1.40  (** Sledgehammer commands **)
    1.41  
    1.42  fun add_to_relevance_override ns : relevance_override =
    1.43 @@ -357,8 +331,4 @@
    1.44        "set and display the default parameters for Sledgehammer" Keyword.thy_decl
    1.45        parse_sledgehammer_params_command
    1.46  
    1.47 -val setup =
    1.48 -  neg_clausify_setup
    1.49 -  #> clausify_setup
    1.50 -
    1.51  end;