# HG changeset patch
# User blanchet
# Date 1336395049 -7200
# Node ID e389889da7df255d2e7df5679dd67bb513e78410
# Parent  e3627a83b1141fbc2fc46c970be7217cc5f121d1
prevent spurious timeouts

diff -r e3627a83b114 -r e389889da7df src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Mon May 07 12:20:55 2012 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon May 07 14:50:49 2012 +0200
@@ -34,7 +34,7 @@
 "add_swap = (\<lambda>x y. y + x)"
 
 lemma "add_swap m n = n + m"
-sledgehammer [expect = some]
+sledgehammer [expect = some] (add_swap_def)
 by (metis_exhaust add_swap_def)
 
 definition "A = {xs\<Colon>'a list. True}"