# HG changeset patch
# User wenzelm
# Date 1003185330 -7200
# Node ID 12a0fb3ac3664c57576a8b206f056320ab96a8bd
# Parent  ad12f865b70d5672dc2f3f6d91b02c26f3b2d2b1
be more careful about token class markers;

diff -r ad12f865b70d -r 12a0fb3ac366 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Oct 16 00:35:03 2001 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Oct 16 00:35:30 2001 +0200
@@ -99,7 +99,10 @@
 
 (** term_to_ast **)
 
-fun mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
+fun mark_freevars ((t as Const (c, _)) $ u) =
+      if c mem_string TokenTrans.standard_token_markers then (t $ u)
+      else t $ mark_freevars u
+  | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
   | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
   | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
   | mark_freevars (t as Var (xi, T)) =
diff -r ad12f865b70d -r 12a0fb3ac366 src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Tue Oct 16 00:35:03 2001 +0200
+++ b/src/Pure/Syntax/token_trans.ML	Tue Oct 16 00:35:30 2001 +0200
@@ -15,6 +15,7 @@
 signature TOKEN_TRANS =
 sig
   include TOKEN_TRANS0
+  val standard_token_markers: string list
   val normal: string
   val bold: string
   val underline: string
@@ -53,6 +54,7 @@
 val standard_token_classes =
   ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];
 
+val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
 
 
 (** xterm output **)