src/Pure/pure_thy.ML
changeset 19577 fdb3642feb49
parent 19482 9f11af8f7ef9
child 19629 c107e7a79559
--- a/src/Pure/pure_thy.ML	Fri May 05 21:59:44 2006 +0200
+++ b/src/Pure/pure_thy.ML	Fri May 05 21:59:45 2006 +0200
@@ -569,6 +569,7 @@
     ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
     ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
     ("_idtypdummy", "type => idt",        Mixfix ("'_()\\<Colon>_", [], 0)),
+    ("_type_constraint_", "'a",           NoSyn),
     ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
     ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),