diff -r 04dd306fdb3c -r d23a3a4d1849 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri Apr 30 18:12:41 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Fri Apr 30 18:29:04 2010 +0200
@@ -711,7 +711,7 @@
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-sledgehammer
+(*sledgehammer*)
 proof -
   assume A1: "X \<in> synth (analz H)"
   have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"