made "clausify" attribute a legacy feature;
seems to have ever only been a debugging feature
--- 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 **)