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;