--- a/src/HOL/HOL.thy Sat Mar 05 19:14:04 2016 +0100
+++ b/src/HOL/HOL.thy Sat Mar 05 19:58:56 2016 +0100
@@ -155,7 +155,7 @@
Ex (binder "EX " 10) and
Ex1 (binder "EX! " 10)
-notation (HOL)
+notation (input)
All (binder "! " 10) and
Ex (binder "? " 10) and
Ex1 (binder "?! " 10)