# HG changeset patch
# User blanchet
# Date 1284471597 -7200
# Node ID 61f0d36840c5fb28eecfa8c6e4ee7d2decea55f0
# Parent  1c4e38d635e18103735ad0bbe5c112a54f19634b
Sledgehammer should be called in "prove" mode;
otherwise the proof text won't fit into the proof document

diff -r 1c4e38d635e1 -r 61f0d36840c5 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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