1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 28 05:52:28 2011 -0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 28 10:42:24 2011 +0200
     1.3 @@ -1915,20 +1915,7 @@
     1.4  
     1.5  subsection{* Explicit vector construction from lists. *}
     1.6  
     1.7 -primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
     1.8 -where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
     1.9 -
    1.10 -lemma from_nat [simp]: "from_nat = of_nat"
    1.11 -by (rule ext, induct_tac x, simp_all)
    1.12 -
    1.13 -primrec
    1.14 -  list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
    1.15 -where
    1.16 -  "list_fun n [] = (\<lambda>x. 0)"
    1.17 -| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
    1.18 -
    1.19 -definition "vector l = (\<chi> i. list_fun 1 l i)"
    1.20 -(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
    1.21 +definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
    1.22  
    1.23  lemma vector_1: "(vector[x]) $1 = x"
    1.24    unfolding vector_def by simp