diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Fun.thy Mon Sep 01 16:17:46 2014 +0200
@@ -585,7 +585,7 @@
"f(x:=y)" == "CONST fun_upd f x y"
(* Hint: to define the sum of two functions (or maps), use case_sum.
- A nice infix syntax could be defined (in Datatype.thy or below) by
+ A nice infix syntax could be defined by
notation
case_sum (infixr "'(+')"80)
*)