clarified proof_result: finish proof formally via head tr, not end_tr;

--- a/src/Pure/Isar/toplevel.ML	Wed Apr 11 14:20:51 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 11 15:02:48 2012 +0200
@@ -691,7 +691,8 @@
               in (result, presentation_context_of result_state) end))
         #-> Result.put;
 
-      val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+      val st'' = st'
+        |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
       val result =
         Result.get (presentation_context_of st'')
         |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);