--- a/src/Pure/pure_thy.ML Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/pure_thy.ML Sat Nov 29 13:37:13 2008 +0100
@@ -321,6 +321,7 @@
("", typ "var => logic", Delimfix "_"),
("_DDDOT", typ "logic", Delimfix "..."),
("_constify", typ "num => num_const", Delimfix "_"),
+ ("_constify", typ "float => float_const", Delimfix "_"),
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),