src/Pure/pure_thy.ML
changeset 38975 ef13a2cc97be
parent 37216 3165bc303f66
child 39507 839873937ddd
     1.1 --- a/src/Pure/pure_thy.ML	Wed Sep 01 15:01:23 2010 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Wed Sep 01 17:59:06 2010 +0200
     1.3 @@ -320,6 +320,7 @@
     1.4      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     1.5      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     1.6      ("_update_name", typ "idt",                        NoSyn),
     1.7 +    (Syntax.constrainAbsC, typ "'a",                   NoSyn),
     1.8      (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     1.9      (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
    1.10      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),