--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Mar 18 12:58:52 2010 +0100
@@ -326,7 +326,7 @@
val multi_base_blacklist =
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
- "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "noatp" *)
+ "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "no_atp" *)
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);