diff -r 689f5dae1f41 -r e31d63c66f55 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 14:28:09 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 14:44:53 2009 -0700
@@ -969,8 +969,8 @@
   "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
 
 definition
-  indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
-  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
+  indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
+  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
 
 text{* Prove That They are all nets. *}