Sledgehammer should be called in "prove" mode;
otherwise the proof text won't fit into the proof document

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 14 14:47:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 14 15:39:57 2010 +0200
@@ -438,6 +438,7 @@
     0 => (priority "No subgoal!"; (false, state))
   | n =>
     let
+      val _ = Proof.assert_backward state
       val thy = Proof.theory_of state
       val timer = Timer.startRealTimer ()
       val _ = () |> not blocking ? kill_atps