--- 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)) =
--- 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 **)