# HG changeset patch
# User blanchet
# Date 1325510817 -3600
# Node ID 291c14a01b6d1aebd9d4318d6761bc69b09a4c5b
# Parent  1613933e412c3f4e1ad1ec30214b11ae7500aa18
reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter

diff -r 1613933e412c -r 291c14a01b6d src/HOL/Metis_Examples/Proxies.thy
--- 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"