changeset 31326 | deddd77112b7 |
parent 30587 | ad19c99529eb |
child 31335 | ba5b7749fa61 |
--- a/src/Pure/General/ROOT.ML Mon Jun 01 15:26:00 2009 +0200 +++ b/src/Pure/General/ROOT.ML Mon Jun 01 15:26:00 2009 +0200 @@ -16,10 +16,6 @@ use "position.ML"; use "symbol_pos.ML"; use "antiquote.ML"; -use "../ML/ml_lex.ML"; -use "../ML/ml_parse.ML"; -use "secure.ML"; - use "integer.ML"; use "stack.ML"; use "queue.ML"; @@ -34,7 +30,6 @@ use "path.ML"; use "url.ML"; use "buffer.ML"; -use "file.ML"; use "xml.ML"; use "yxml.ML";