src/Pure/Tools/ml_statistics.scala
changeset 57612 990ffb84489b
parent 53189 ee8b8dafef0e
child 57869 9665f79a7181
     1.1 --- a/src/Pure/Tools/ml_statistics.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Pure/Tools/ml_statistics.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4  
     1.5    def show_standard_frames(): Unit =
     1.6      ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
     1.7 -      Swing_Thread.later {
     1.8 +      GUI_Thread.later {
     1.9          new Frame {
    1.10            iconImage = GUI.isabelle_image()
    1.11            title = name