# HG changeset patch
# User paulson
# Date 845369757 -7200
# Node ID e8544d73a7aa37dbb5461acb4a64373c30e2a494
# Parent  2061df98aab5cf6a699510b992b7c8dc8cf28424
changed prettyprinting of ==>

diff -r 2061df98aab5 -r e8544d73a7aa src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Oct 15 10:46:42 1996 +0200
+++ b/src/Pure/sign.ML	Tue Oct 15 10:55:57 1996 +0200
@@ -579,7 +579,7 @@
   |> add_consts
    [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
-    ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
+    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("TYPE", "'a itself", NoSyn)]
   |> add_name "ProtoPure";