# HG changeset patch
# User wenzelm
# Date 1365088611 -7200
# Node ID 81f8da412b7f53e7daf6f5c91e63baa813febf0a
# Parent  6a1e40f9dd55be6195076a99af1ed7874aaa1fb8
tuned imports;

diff -r 6a1e40f9dd55 -r 81f8da412b7f src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Apr 04 12:06:23 2013 +0200
+++ b/src/Pure/General/pretty.scala	Thu Apr 04 17:16:51 2013 +0200
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import java.awt.FontMetrics
-
-
 object Pretty
 {
   /* spaces */