actually declare "_constrainAbs" as @{syntax_const};
authorwenzelm
Wed, 01 Sep 2010 17:59:06 +0200
changeset 38975 ef13a2cc97be
parent 38974 e109feb514a8
child 38976 a4a465dc89d9
actually declare "_constrainAbs" as @{syntax_const};
src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Sep 01 15:01:23 2010 +0200
+++ b/src/Pure/pure_thy.ML	Wed Sep 01 17:59:06 2010 +0200
@@ -320,6 +320,7 @@
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
+    (Syntax.constrainAbsC, typ "'a",                   NoSyn),
     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),