# HG changeset patch
# User blanchet
# Date 1357381449 -3600
# Node ID 07dfdf72ab757c47253d6101602f4991ca5b51f5
# Parent  6b232d76cbc991623ee2e3bf836a9ff195b60d17
tuned blacklisting in relevance filter

diff -r 6b232d76cbc9 -r 07dfdf72ab75 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 04 21:56:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 05 11:24:09 2013 +0100
@@ -141,10 +141,11 @@
 
 (* Reject theorems with names like "List.filter.filter_list_def" or
   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
-fun is_package_def a =
-  let val names = Long_Name.explode a in
-    (length names > 2 andalso not (hd names = "local") andalso
-     String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
+fun is_package_def s =
+  let val ss = Long_Name.explode s in
+    length ss > 2 andalso not (hd ss = "local") andalso
+    exists (fn suf => String.isSuffix suf s)
+           ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   end
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
@@ -189,10 +190,10 @@
 
 (* FIXME: Ad hoc list *)
 val technical_prefixes =
-  ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson",
-   "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck",
-   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence",
-   "Sledgehammer", "SMT"]
+  ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence",
+   "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence",
+   "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
+   "Random_Sequence", "Sledgehammer", "SMT"]
   |> map (suffix Long_Name.separator)
 
 fun has_technical_prefix s =