# HG changeset patch
# User paulson
# Date 1139484002 -3600
# Node ID bc23b1d1ddea6c2d2448e3fa5d1f2bc82a27aeb8
# Parent  4301eb0f051fdde3a9d098c4e03dfa604f6e2060
blacklist tweaks

diff -r 4301eb0f051f -r bc23b1d1ddea src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Feb 09 12:14:39 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Feb 09 12:20:02 2006 +0100
@@ -23,9 +23,9 @@
   FIXME: this blacklist needs to be maintained using theory data and added to using
   an attribute.*)
 val blacklist = ref
-  ["Datatype.not_None_eq_iff2",
-   "Datatype.not_Some_eq_D",
-   "Datatype.not_Some_eq",
+  ["Datatype.not_None_eq",    (*Says everything is None or Some. Probably prolific.*)
+   "Datatype.not_Some_eq_D",  (*Says everything is None or Some. Probably prolific.*)
+   "Datatype.not_Some_eq",    (*Says everything is None or Some. Probably prolific.*)
    "Datatype.option.size_1",
    "Datatype.option.size_2",
    "Datatype.prod.size",
@@ -57,6 +57,7 @@
    "IntDiv.zero_less_zpower_abs_iff",
    "List.append_eq_append_conv",
    "List.Cons_in_lex",
+   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
    "List.in_listsD",
    "List.in_listsI",
    "List.lists.Cons",