SynExt.standard_token_markers
authorwenzelm
Sat, 23 Apr 2005 19:51:35 +0200
changeset 15834 a5166d054683
parent 15833 78109c7012ed
child 15835 fdf678bec567
SynExt.standard_token_markers
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)