--- 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