diff -r d0e8cb55ee7b -r 497474b69c86 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Dec 17 17:57:52 2007 +0100
+++ b/src/HOL/Map.thy	Mon Dec 17 18:01:51 2007 +0100
@@ -23,7 +23,7 @@
   "empty == %x. None"
 
 definition
-  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)"  (infixl "o'_m" 55) where
+  map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)"  (infixl "o'_m" 55) where
   "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
 
 notation (xsymbols)