src/HOL/SEQ.thy

--- a/src/HOL/SEQ.thy	Tue Jun 02 23:06:05 2009 -0700
+++ b/src/HOL/SEQ.thy	Tue Jun 02 23:31:03 2009 -0700
@@ -24,7 +24,7 @@
   [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
 
 definition
-  lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
+  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
     --{*Standard definition of limit using choice operator*}
   "lim X = (THE L. X ----> L)"