# HG changeset patch
# User wenzelm
# Date 1114278695 -7200
# Node ID a5166d054683d34ac975b4dc84cc3500af09dec8
# Parent  78109c7012ed6650dd85118b6f13719877939a5d
SynExt.standard_token_markers

diff -r 78109c7012ed -r a5166d054683 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Apr 23 19:51:24 2005 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Apr 23 19:51:35 2005 +0200
@@ -106,7 +106,7 @@
 (** term_to_ast **)
 
 fun mark_freevars ((t as Const (c, _)) $ u) =
-      if c mem_string TokenTrans.standard_token_markers then (t $ u)
+      if c mem_string SynExt.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)