diff -r df958c7afe50 -r 78109c7012ed src/Pure/Syntax/ROOT.ML --- 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;