diff -r b378b6faf4a7 -r 2c116016f95d src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Jan 26 15:33:51 2004 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Jan 27 08:15:10 2004 +0100
@@ -269,7 +269,7 @@
   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
   ("=?=",      "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>\\<^sup>?", 2)),
   ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
-  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
 
 end;