src/Pure/Syntax/ROOT.ML
changeset 15833 78109c7012ed
parent 14981 e73f8140af78
--- a/src/Pure/Syntax/ROOT.ML	Sat Apr 23 19:51:11 2005 +0200
+++ b/src/Pure/Syntax/ROOT.ML	Sat Apr 23 19:51:24 2005 +0200
@@ -6,7 +6,6 @@
 *)
 
 use "lexicon.ML";
-use "token_trans.ML";
 use "ast.ML";
 use "syn_ext.ML";
 use "parser.ML";
@@ -18,7 +17,6 @@
 
 (*hiding private stuff*)
 structure Lexicon = Hidden;
-structure TokenTrans = Hidden;
 structure Ast = Hidden;
 structure SynExt = Hidden;
 structure Parser = Hidden;