--- a/src/HOL/RealDef.thy Tue Jun 16 14:56:59 2009 +0200
+++ b/src/HOL/RealDef.thy Tue Jun 16 16:26:40 2009 +0200
@@ -1169,7 +1169,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;
@@ -1181,8 +1181,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