# HG changeset patch
# User blanchet
# Date 1282579471 -7200
# Node ID f9edc593e929d725b37be48e9c56f30b3f5bd21a
# Parent  634a6d400c2e8e1ce606428e2c7e8d5e3144d339
no need for "eq" facts -- good old "=" is good enough for us

diff -r 634a6d400c2e -r f9edc593e929 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 17:53:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 18:04:31 2010 +0200
@@ -386,7 +386,7 @@
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
   ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
-   "split_asm", "cases", "ext_cases"]
+   "split_asm", "cases", "ext_cases", "eq"]
 
 val max_lambda_nesting = 3