diff -r 786edc984c98 -r a5c9002bc54d src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Fri Feb 14 07:53:46 2014 +0100 +++ b/src/HOL/Predicate.thy Fri Feb 14 07:53:46 2014 +0100 @@ -396,7 +396,7 @@ "eval (map f P) = (\x\{x. eval P x}. (\y. f x = y))" by (auto simp add: map_def comp_def) -enriched_type map: map +functor map: map by (rule ext, rule pred_eqI, auto)+