--- a/src/Pure/pure_thy.ML Mon Jan 16 20:32:33 2012 +0100
+++ b/src/Pure/pure_thy.ML Mon Jan 16 21:50:15 2012 +0100
@@ -125,9 +125,12 @@
("", typ "var => logic", Delimfix "_"),
("_DDDOT", typ "logic", Delimfix "..."),
("_strip_positions", typ "'a", NoSyn),
- ("_constify", typ "num_token => num_const", Delimfix "_"),
- ("_constify", typ "float_token => float_const", Delimfix "_"),
- ("_constify", typ "xnum_token => xnum_const", Delimfix "_"),
+ ("_position", typ "num_token => num_position", Delimfix "_"),
+ ("_position", typ "float_token => float_position", Delimfix "_"),
+ ("_position", typ "xnum_token => xnum_position", Delimfix "_"),
+ ("_constify", typ "num_position => num_const", Delimfix "_"),
+ ("_constify", typ "float_position => float_const", Delimfix "_"),
+ ("_constify", typ "xnum_position => xnum_const", Delimfix "_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
("_indexvar", typ "index", Delimfix "'\\<index>"),