src/Pure/pure_thy.ML
changeset 52211 66bc827e37f8
parent 52161 51eca565b153
child 53171 a5e54d4d9081
     1.1 --- a/src/Pure/pure_thy.ML	Tue May 28 16:29:11 2013 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue May 28 23:06:32 2013 +0200
     1.3 @@ -81,6 +81,7 @@
     1.4      ("",            typ "prop' => prop'",              Delimfix "'(_')"),
     1.5      ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
     1.6      ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
     1.7 +    ("_ignore_type", typ "'a",                         NoSyn),
     1.8      ("",            typ "tid_position => type",        Delimfix "_"),
     1.9      ("",            typ "tvar_position => type",       Delimfix "_"),
    1.10      ("",            typ "type_name => type",           Delimfix "_"),