# HG changeset patch
# User wenzelm
# Date 1354307315 -3600
# Node ID 1426d478ccda46319c5a2098c293f043eea040c0
# Parent  62edbd5c95cc3bbda89bc8037c0ef0913b159afa
tuned import;

diff -r 62edbd5c95cc -r 1426d478ccda src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Fri Nov 30 17:53:32 2012 +0100
+++ b/src/Pure/General/time.scala	Fri Nov 30 21:28:35 2012 +0100
@@ -8,6 +8,9 @@
 package isabelle
 
 
+import java.util.Locale
+
+
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
@@ -24,7 +27,7 @@
   def is_relevant: Boolean = ms >= 1
 
   override def toString =
-    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+    String.format(Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
 
   def message: String = toString + "s"
 }
diff -r 62edbd5c95cc -r 1426d478ccda src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Nov 30 17:53:32 2012 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Nov 30 21:28:35 2012 +0100
@@ -9,7 +9,6 @@
 
 import java.lang.System
 import java.util.regex.Pattern
-import java.util.Locale
 import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
   BufferedWriter, OutputStreamWriter, IOException, FileInputStream, BufferedInputStream}
 import java.awt.{GraphicsEnvironment, Font}