diff -r 5d3c022cbf97 -r 681ffad36776 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Mon Jul 09 23:12:29 2007 +0200 +++ b/src/Pure/General/ROOT.ML Mon Jul 09 23:12:31 2007 +0200 @@ -20,7 +20,6 @@ use "name_space.ML"; use "seq.ML"; use "susp.ML"; -use "position.ML"; use "path.ML"; use "url.ML"; use "file.ML";