denominator should not be zero

--- a/src/HOL/Rational.thy	Tue Jun 16 14:56:59 2009 +0200
+++ b/src/HOL/Rational.thy	Tue Jun 16 16:26:40 2009 +0200
@@ -1048,7 +1048,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_rat r)
   end;
@@ -1060,8 +1060,7 @@
 consts_code
   "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
 attach {*
-fun rat_of_int 0 = (0, 0)
-  | rat_of_int i = (i, 1);
+fun rat_of_int i (i, 1);
 *}
 
 end

--- 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