src/Pure/pure_thy.ML
changeset 45389 bc0d50f8ae19
parent 44433 9fbee4aab115
child 45490 20c8c0cca555
     1.1 --- a/src/Pure/pure_thy.ML	Mon Nov 07 16:39:14 2011 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Mon Nov 07 16:41:16 2011 +0100
     1.3 @@ -127,8 +127,6 @@
     1.4      ("_strip_positions", typ "'a", NoSyn),
     1.5      ("_constify",   typ "num => num_const",            Delimfix "_"),
     1.6      ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     1.7 -    ("_index1",     typ "index",                       Delimfix "\\<^sub>1"),
     1.8 -    ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     1.9      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    1.10      ("_indexdefault", typ "index",                     Delimfix ""),
    1.11      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),