clarified proof_result: finish proof formally via head tr, not end_tr;
authorwenzelm
Wed, 11 Apr 2012 15:02:48 +0200
changeset 4829645e570742e73
parent 48295 57ff63a52c53
child 48297 26c1a97c7784
clarified proof_result: finish proof formally via head tr, not end_tr;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 11 14:20:51 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 11 15:02:48 2012 +0200
     1.3 @@ -691,7 +691,8 @@
     1.4                in (result, presentation_context_of result_state) end))
     1.5          #-> Result.put;
     1.6  
     1.7 -      val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
     1.8 +      val st'' = st'
     1.9 +        |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.10        val result =
    1.11          Result.get (presentation_context_of st'')
    1.12          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);