diff -r dd58f13a8eb4 -r eb85850d3eb7 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/FOL/IFOL.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -45,7 +45,7 @@
 
 
 abbreviation
-  not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
+  not_equal :: "['a, 'a] => o"  (infixl "~=" 50) where
   "x ~= y == ~ (x = y)"
 
 notation (xsymbols)