# HG changeset patch
# User wenzelm
# Date 1244571501 -7200
# Node ID 73adb1fa8553db1b8bb3e14ff0b7c458a8d563c6
# Parent  0a99c871631240c1caea6e8fd359a5acc25dc82d
tuned;

diff -r 0a99c8716312 -r 73adb1fa8553 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Tue Jun 09 01:32:57 2009 +0200
+++ b/src/Pure/General/yxml.scala	Tue Jun 09 20:18:21 2009 +0200
@@ -6,8 +6,6 @@
 
 package isabelle
 
-import java.util.regex.Pattern
-
 
 object YXML {