author | wenzelm |
Tue, 26 Feb 2013 13:27:24 +0100 | |
changeset 51282 | 3d3c1ea0a401 |
parent 51281 | c05f7e1dd602 |
child 51283 | fefd07697979 |
--- a/src/Pure/Isar/toplevel.ML Tue Feb 26 13:05:48 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Feb 26 13:27:24 2013 +0100 @@ -637,8 +637,7 @@ local fun timing_message tr (t: Timing.timing) = - if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr)) - then + if Timing.is_relevant_time (#elapsed t) then (case approximative_id tr of SOME id => (Output.protocol_message