reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter

--- a/src/HOL/Metis_Examples/Proxies.thy	Mon Jan 02 14:12:20 2012 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jan 02 14:26:57 2012 +0100
@@ -40,7 +40,8 @@
 definition "A = {xs\<Colon>'a list. True}"
 
 lemma "xs \<in> A"
-sledgehammer(* FIXME [expect = some] *)
+(* The "add:" argument is unfortunate. *)
+sledgehammer [expect = some] (add: A_def mem_Collect_eq)
 by (metis_exhaust A_def mem_Collect_eq)
 
 definition "B (y::int) \<equiv> y \<le> 0"