diff -r 9baa48bad81c -r 74fc28c5d68c src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Wed Jun 03 10:02:59 2009 -0700
+++ b/src/HOL/RealVector.thy	Wed Jun 03 10:29:11 2009 -0700
@@ -537,7 +537,7 @@
 definition dist_real_def:
   "dist x y = \<bar>x - y\<bar>"
 
-definition topo_real_def:
+definition topo_real_def [code del]:
   "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
 
 instance