# HG changeset patch
# User wenzelm
# Date 1208442648 -7200
# Node ID a079f8f0080b05e2d0c1f5a74bfd1b910869dfd8
# Parent  341c4d51d1c215753945304f10c501237a991cb7
added markup for fixed variables (local constants);

diff -r 341c4d51d1c2 -r a079f8f0080b src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Apr 17 16:30:47 2008 +0200
+++ b/src/Pure/General/markup.ML	Thu Apr 17 16:30:48 2008 +0200
@@ -32,6 +32,7 @@
   val fbreakN: string val fbreak: T
   val classN: string val class: string -> T
   val tyconN: string val tycon: string -> T
+  val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
   val axiomN: string val axiom: string -> T
   val tfreeN: string val tfree: T
@@ -132,6 +133,7 @@
 
 val (classN, class) = markup_string "class" nameN;
 val (tyconN, tycon) = markup_string "tycon" nameN;
+val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "const" nameN;
 val (axiomN, axiom) = markup_string "axiom" nameN;