--- a/src/HOL/Library/OptionalSugar.thy Wed Sep 09 11:24:34 2015 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Wed Sep 09 14:47:41 2015 +0200
@@ -48,14 +48,13 @@
"_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
(* type constraints with spacing *)
+no_syntax (output)
+ "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3)
-no_syntax (xsymbols output)
- "_constrain" :: "logic => type => logic" ("_\<Colon>_" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_\<Colon>_" [4, 0] 3)
-
-syntax (xsymbols output)
- "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_ \<Colon> _" [4, 0] 3)
+syntax (output)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
(* sorts as intersections *)