diff -r bcb696533579 -r 1220ecb81e8f src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Thu Aug 18 13:25:17 2011 +0200
+++ b/src/HOL/RealDef.thy	Thu Aug 18 13:55:26 2011 +0200
@@ -121,7 +121,7 @@
 subsection {* Cauchy sequences *}
 
 definition
-  cauchy :: "(nat \<Rightarrow> rat) set"
+  cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
 where
   "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"