src/Pure/pure_thy.ML
changeset 62107 f74a33b14200
parent 61957 301833d9013a
child 62529 8b7bdfc09f3b
     1.1 --- a/src/Pure/pure_thy.ML	Fri Jan 08 20:06:48 2016 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 09 12:35:07 2016 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     1.5      ("_indexdefault", typ "index",                     Delimfix ""),
     1.6      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     1.7 -    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     1.8 +    ("_struct",     typ "index => logic",              NoSyn),
     1.9      ("_update_name", typ "idt",                        NoSyn),
    1.10      ("_constrainAbs", typ "'a",                        NoSyn),
    1.11      ("_position_sort", typ "tid => tid_position",      Delimfix "_"),