diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Dec 21 16:14:46 2010 +0100 +++ b/src/HOL/Product_Type.thy Tue Dec 21 17:52:23 2010 +0100 @@ -834,8 +834,8 @@ "map_pair f g (a, b) = (f a, g b)" by (simp add: map_pair_def) -type_lifting map_pair - by (simp_all add: split_paired_all) +type_lifting map_pair: map_pair + by (auto simp add: split_paired_all intro: ext) lemma fst_map_pair [simp]: "fst (map_pair f g x) = f (fst x)"