# HG changeset patch
# User blanchet
# Date 1275657706 -7200
# Node ID 2f45de0a8513e0f8c4d45941588afdfcea0b697a
# Parent  bf5d936bb985ee3c410742e9c85e9c0cb8311332
made "neg_clausify" a legacy feature

diff -r bf5d936bb985 -r 2f45de0a8513 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:09:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:21:46 2010 +0200
@@ -28,8 +28,11 @@
 
 val neg_clausify_setup =
   Method.setup @{binding neg_clausify}
-               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
-               "conversion of goal to negated conjecture clauses"
+               (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 **)