# HG changeset patch
# User wenzelm
# Date 1230921494 -3600
# Node ID 592503fd6dada4d068d6e0500e8bf7f537e2ec7f
# Parent  6337d1cb2ba04e95160997d2cdee22d1a6b5f2a2
more detailed inner token markup;

diff -r 6337d1cb2ba0 -r 592503fd6dad src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Jan 02 19:38:13 2009 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Jan 02 19:38:14 2009 +0100
@@ -58,9 +58,9 @@
   | T.Ident         => Markup.ident
   | T.LongIdent     => Markup.ident
   | T.SymIdent      => Markup.ident
-  | T.Var           => Markup.ident
-  | T.TypeIdent     => Markup.ident
-  | T.TypeVar       => Markup.ident
+  | T.Var           => Markup.var
+  | T.TypeIdent     => Markup.tfree
+  | T.TypeVar       => Markup.tvar
   | T.Nat           => Markup.ident
   | T.String        => Markup.string
   | T.AltString     => Markup.altstring