diff -r 22bbc1676768 -r b55686a7b22c src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Maybe.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -13,6 +13,6 @@
   "option_bind m f == case m of None => None | Some r => f r"
 
 syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "option_bind E (%P.F)"
+translations "P := E; F" == "option_bind E (%P. F)"
 
 end