# HG changeset patch
# User haftmann
# Date 1324739698 -3600
# Node ID 989b1eede03cde077f49b5ff2650ee8e752bdffc
# Parent  4c629115e3ab541715d21f0b6d096ea4f222aec0
dropped references to obsolete facts `mem_def` and `Collect_def`

diff -r 4c629115e3ab -r 989b1eede03c src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Dec 24 16:14:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Dec 24 16:14:58 2011 +0100
@@ -283,8 +283,8 @@
    by treating them more or less as if they were built-in but add their
    definition at the end. *)
 val set_consts =
-  [(@{const_name Collect}, @{thms Collect_def}),
-   (@{const_name Set.member}, @{thms mem_def})]
+  [(@{const_name Collect}, []),
+   (@{const_name Set.member}, [])]
 
 val is_set_const = AList.defined (op =) set_consts