--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 12 08:35:56 2014 +0100
@@ -766,7 +766,7 @@
bs: "set bs = Basis" "distinct bs"
by (metis finite_distinct_list)
from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
- def y \<equiv> "list_rec
+ def y \<equiv> "rec_list
(s j)
(\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"