     1.1 --- a/src/Pure/pure_thy.ML	Tue Dec 23 13:20:34 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Dec 23 19:27:42 2008 +0100
     1.3 @@ -322,7 +322,7 @@
     1.4      ("",            typ "var => logic",                Delimfix "_"),
     1.5      ("_DDDOT",      typ "logic",                       Delimfix "..."),
     1.6      ("_constify",   typ "num => num_const",            Delimfix "_"),
     1.7 -    ("_constify",   typ "float => float_const",        Delimfix "_"),
     1.8 +    ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     1.9      ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
    1.10      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    1.11      ("_indexdefault", typ "index",                     Delimfix ""),
changeset 29156	89f76a58a378
parent 29007	c9cdb569487a
child 29421	b28bf19d7ab9