--- a/src/Pure/pure_thy.ML Tue Aug 23 19:49:21 2011 +0200
+++ b/src/Pure/pure_thy.ML Mon Aug 22 23:39:05 2011 +0200
@@ -127,6 +127,7 @@
("_strip_positions", typ "'a", NoSyn),
("_constify", typ "num => num_const", Delimfix "_"),
("_constify", typ "float_token => float_const", Delimfix "_"),
+ ("_index1", typ "index", Delimfix "\\<^sub>1"),
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),