# HG changeset patch
# User blanchet
# Date 1443813711 -7200
# Node ID 07eb540da4ab1295786f085cc0d24c769018648f
# Parent  570dae974f6460757e5e58bc78a00a71239f1ee9
adapted example

diff -r 570dae974f64 -r 07eb540da4ab src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Fri Oct 02 21:16:16 2015 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Fri Oct 02 21:21:51 2015 +0200
@@ -14,8 +14,8 @@
 imports Type_Encodings
 begin
 
-sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
-                     preplay_timeout = 0, dont_minimize]
+sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
+  dont_minimize]
 
 text {* Extensionality and set constants *}