1.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -95,8 +95,8 @@
     1.4  lemma PAIR: "(fst x,snd x) = x"
     1.5    by simp
     1.6  
     1.7 -lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
     1.8 -  by (simp add: prod_fun_def split_def)
     1.9 +lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
    1.10 +  by (simp add: map_pair_def split_def)
    1.11  
    1.12  lemma pair_case_def: "split = split"
    1.13    ..;