# HG changeset patch
# User wenzelm
# Date 1267614227 -3600
# Node ID e6c03f397eb83652e459617e6d851b49d21d6de6
# Parent  a4babce15c67f7e4669f6c3202148efa7d225b61
mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;

diff -r a4babce15c67 -r e6c03f397eb8 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Mar 03 12:02:59 2010 +0100
+++ b/src/Pure/Syntax/printer.ML	Wed Mar 03 12:03:47 2010 +0100
@@ -114,15 +114,17 @@
     val {structs, fixes} = idents;
 
     fun mark_atoms ((t as Const (c, T)) $ u) =
-          if member (op =) consts c then (t $ u)
-          else Const (Lexicon.mark_const c, T) $ mark_atoms u
+          if member (op =) SynExt.standard_token_markers c
+          then t $ u else mark_atoms t $ mark_atoms u
       | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
       | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
-      | mark_atoms (Const (c, T)) = Const (Lexicon.mark_const c, T)
+      | mark_atoms (t as Const (c, T)) =
+          if member (op =) consts c then t
+          else Const (Lexicon.mark_const c, T)
       | mark_atoms (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
             if i = 0 andalso member (op =) fixes x then
-              Term.Const (Lexicon.mark_fixed x, T)
+              Const (Lexicon.mark_fixed x, T)
             else if i = 1 andalso not show_structs then
               Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
             else Lexicon.const "_free" $ t