diff -r 8369f3f4bb4f -r 0487add593b5 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 19 13:21:28 1996 +0100
+++ b/src/Pure/sign.ML	Tue Nov 19 14:20:02 1996 +0100
@@ -616,9 +616,11 @@
   |> add_consts
    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
-    ("==>", "[prop, prop] => prop", InfixrName ("==>", 1)),
+    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("TYPE", "'a itself", NoSyn)]
+  |> add_syntax
+   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   |> add_name "ProtoPure";
 
 val pure = proto_pure