src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:21:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:41:27 2010 +0200
@@ -44,7 +44,9 @@
                   end))
 
 val clausify_setup =
-  Attrib.setup @{binding clausify} parse_clausify_attribute
+  Attrib.setup @{binding clausify}
+               (parse_clausify_attribute
+                o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
                "conversion of theorem to clauses"
 
 (** Sledgehammer commands **)