# HG changeset patch
# User blanchet
# Date 1335692673 -7200
# Node ID 1d25deb1f185667e7a979efb2e85e8753ef2bee9
# Parent  4ad2b7ccd0ff8184efaa82c43479090cbb630748
Sledgehammer can do it

diff -r 4ad2b7ccd0ff -r 1d25deb1f185 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Sun Apr 29 09:25:54 2012 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Sun Apr 29 11:44:33 2012 +0200
@@ -27,14 +27,14 @@
 by (metis_exhaust inc_def plus_1_not_0)
 
 lemma "inc = (\<lambda>y. y + 1)"
-sledgehammer [expect = some] (inc_def)
+sledgehammer [expect = some]
 by (metis_exhaust inc_def)
 
 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "add_swap = (\<lambda>x y. y + x)"
 
 lemma "add_swap m n = n + m"
-sledgehammer [expect = some] (add_swap_def)
+sledgehammer [expect = some]
 by (metis_exhaust add_swap_def)
 
 definition "A = {xs\<Colon>'a list. True}"