diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -18,7 +18,7 @@
 
 (* aligning equations *)
 notation (tab output)
-  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
+  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
 
 (* Let *)