diff -r b3fc3a62247a -r 3ef9489eeef5 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/General/markup.ML	Sat Nov 29 13:37:13 2008 +0100
@@ -53,6 +53,7 @@
   val boundN: string val bound: T
   val varN: string val var: T
   val numN: string val num: T
+  val floatN: string val float: T
   val xnumN: string val xnum: T
   val xstrN: string val xstr: T
   val literalN: string val literal: T
@@ -203,6 +204,7 @@
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
 val (numN, num) = markup_elem "num";
+val (floatN, float) = markup_elem "float";
 val (xnumN, xnum) = markup_elem "xnum";
 val (xstrN, xstr) = markup_elem "xstr";
 val (literalN, literal) = markup_elem "literal";