src/HOL/Real/RealDef.thy

--- a/src/HOL/Real/RealDef.thy	Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Real/RealDef.thy	Thu Jan 10 19:09:21 2008 +0100
@@ -1051,9 +1051,10 @@
     val g = Integer.gcd p q;
     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')
   in
-    (if one_of [true, false] then p' else ~ p',
-     if p' = 0 then 0 else q')
+    (r, fn () => term_of_real r)
   end;
 *}