--- a/src/Pure/General/timing.ML Mon Aug 14 14:41:22 2017 +0200 +++ b/src/Pure/General/timing.ML Mon Aug 14 15:30:26 2017 +0200 @@ -119,4 +119,3 @@ structure Basic_Timing: BASIC_TIMING = Timing; open Basic_Timing; -