# HG changeset patch
# User haftmann
# Date 1290096076 -3600
# Node ID 6c28ab8b81665d44ccc8fb443d8e81282fba15a3
# Parent  30d512bf47a7d8cbc0abf62a8baaef652520d174
mapper for list type; map_pair replaces prod_fun

diff -r 30d512bf47a7 -r 6c28ab8b8166 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/List.thy	Thu Nov 18 17:01:16 2010 +0100
@@ -881,6 +881,9 @@
   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
 by (induct rule:list_induct2, simp_all)
 
+type_mapper map
+  by simp_all
+
 
 subsubsection {* @{text rev} *}
 
@@ -4300,7 +4303,7 @@
 primrec -- {*The lexicographic ordering for lists of the specified length*}
   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
     "lexn r 0 = {}"
-  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+  | "lexn r (Suc n) = (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
       {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
 
 definition
@@ -4316,7 +4319,7 @@
 apply (induct n, simp, simp)
 apply(rule wf_subset)
  prefer 2 apply (rule Int_lower1)
-apply(rule wf_prod_fun_image)
+apply(rule wf_map_pair_image)
  prefer 2 apply (rule inj_onI, auto)
 done