--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 19:26:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 19:58:43 2010 +0200
@@ -444,7 +444,8 @@
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
if Facts.is_concealed facts name orelse
(respect_no_atp andalso is_package_def name) orelse
- member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name then
I
else
let