# HG changeset patch
# User wenzelm
# Date 1208442653 -7200
# Node ID fc2e7d2f763da1a610aa846325d66b0902e9f5ea
# Parent  ddf6bab64b96cf43dbfe7d7fa7e47a1bf29f6cbe
moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;

diff -r ddf6bab64b96 -r fc2e7d2f763d src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Thu Apr 17 16:30:52 2008 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Thu Apr 17 16:30:53 2008 +0200
@@ -255,7 +255,7 @@
    [],
    [],
    map SynExt.mk_trfun [("fun", K fun_ast_tr')])
-  (map (fn s => ("", s, Output.output_width)) SynExt.standard_token_classes)
+  []
   ([], []);
 
 end;