# HG changeset patch
# User paulson
# Date 1155141548 -7200
# Node ID e42674e0486ea8d582310992f652af40739976db
# Parent  a0f8e89d369d4832f6b03a6f973a0ab2e8137720
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs

diff -r a0f8e89d369d -r e42674e0486e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Aug 09 15:48:51 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Aug 09 18:39:08 2006 +0200
@@ -39,6 +39,7 @@
   val include_all: bool ref
   val run_relevance_filter: bool ref
   val run_blacklist_filter: bool ref
+  val blacklist: string list ref
   val add_all : unit -> unit
   val add_claset : unit -> unit
   val add_simpset : unit -> unit
@@ -304,7 +305,17 @@
   FIXME: this blacklist needs to be maintained using theory data and added to using
   an attribute.*)
 val blacklist = ref
-  ["Datatype.prod.size",
+  ["Datatype.unit.split_asm",         (*These  "unit" thms cause unsound proofs*)
+                               (*Datatype.unit.nchotomy is caught automatically*)
+   "Datatype.unit.induct",
+   "Datatype.unit.inducts",
+   "Datatype.unit.split",
+   "Datatype.unit.splits_1",
+   "Datatype.unit.splits_2",
+   "Product_Type.unit_abs_eta_conv",
+   "Product_Type.unit_induct",
+
+   "Datatype.prod.size",
    "Divides.dvd_0_left_iff",
    "Finite_Set.card_0_eq",
    "Finite_Set.card_infinite",