# HG changeset patch
# User wenzelm
# Date 1114278684 -7200
# Node ID 78109c7012ed6650dd85118b6f13719877939a5d
# Parent  df958c7afe5049b196b940c0232e6c088adf6148
removed token_trans.ML (some content moved to syn_ext.ML);

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;
diff -r df958c7afe50 -r 78109c7012ed src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:11 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:24 2005 +0200
@@ -15,7 +15,6 @@
 
 signature SYNTAX =
 sig
-  include TOKEN_TRANS0
   include AST1
   include LEXICON0
   include SYN_EXT0
@@ -500,9 +499,8 @@
 
 
 
-(** export parts of internal Syntax structures **)
-
-open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
+(*export parts of internal Syntax structures*)
+open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
 
 end;
 
diff -r df958c7afe50 -r 78109c7012ed src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sat Apr 23 19:51:11 2005 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sat Apr 23 19:51:24 2005 +0200
@@ -220,7 +220,7 @@
    [],
    [],
    map SynExt.mk_trfun [("fun", fun_ast_tr')])
-  TokenTrans.token_translation
+  (map (fn s => ("", s, Output.output_width)) SynExt.standard_token_classes)
   ([], []);
 
 end;