diff -r 1db0c8f235fb -r 678d294a563c src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/RealDef.thy	Wed Jun 17 16:56:15 2009 -0700
@@ -1170,7 +1170,7 @@
     val p' = p div g;
     val q' = q div g;
     val r = (if one_of [true, false] then p' else ~ p',
-      if p' = 0 then 0 else q')
+      if p' = 0 then 1 else q')
   in
     (r, fn () => term_of_real r)
   end;
@@ -1182,8 +1182,7 @@
 consts_code
   "of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
 attach {*
-fun real_of_int 0 = (0, 0)
-  | real_of_int i = (i, 1);
+fun real_of_int i = (i, 1);
 *}
 
 end