# HG changeset patch
# User wenzelm
# Date 1334149368 -7200
# Node ID 45e570742e736f8acb068508640515601cd476b2
# Parent  57ff63a52c5374de1efad841c80efb3aabd083f7
clarified proof_result: finish proof formally via head tr, not end_tr;

diff -r 57ff63a52c53 -r 45e570742e73 src/Pure/Isar/toplevel.ML
--- 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'')]);