# HG changeset patch
# User blanchet
# Date 1280426323 -7200
# Node ID 7627881fe9d4104d19fc89d135fe1126665ac113
# Parent  d01b8119b2e0eb94fd72ac20a0ba77d055f827a6
avoid "_def_raw" theorems

diff -r d01b8119b2e0 -r 7627881fe9d4 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- 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