1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Dec 24 16:14:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Dec 24 16:14:58 2011 +0100
     1.3 @@ -283,8 +283,8 @@
     1.4     by treating them more or less as if they were built-in but add their
     1.5     definition at the end. *)
     1.6  val set_consts =
     1.7 -  [(@{const_name Collect}, @{thms Collect_def}),
     1.8 -   (@{const_name Set.member}, @{thms mem_def})]
     1.9 +  [(@{const_name Collect}, []),
    1.10 +   (@{const_name Set.member}, [])]
    1.11  
    1.12  val is_set_const = AList.defined (op =) set_consts
    1.13