speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call

--- a/src/HOL/Metis_Examples/HO_Reas.thy	Tue May 31 19:28:03 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Tue May 31 23:39:27 2011 +0200
@@ -10,7 +10,7 @@
 
 declare [[metis_new_skolemizer]]
 
-sledgehammer_params [prover = e, blocking, timeout = 10]
+sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]
 
 text {* Extensionality and set constants *}
 
@@ -48,7 +48,9 @@
 by linarith
 
 lemma "B \<subseteq> C"
+(* FIXME:
 sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
+*)
 by (metis B_def C_def int_le_0_imp_le_1 predicate1I)