# HG changeset patch
# User paulson
# Date 1169803362 -3600
# Node ID 10278e56874101f7ab92fa0ebc035f431b07de00
# Parent  a63889770d576fadabf374c4dfa011cea5174261
Fixed long-standing, MAJOR bug in "lt"

diff -r a63889770d57 -r 10278e568741 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Fri Jan 26 09:24:35 2007 +0100
+++ b/src/Pure/General/rat.ML	Fri Jan 26 10:22:42 2007 +0100
@@ -87,7 +87,7 @@
   | lt (Rat (true, _, _), Rat (false, _, _)) = false
   | lt (Rat (a, p1, q1), Rat (_, p2, q2)) =
       let val (r1, r2, _) = common (p1, q1, p2, q2)
-      in if a then r1 <= r2 else r2 <= r1 end;
+      in if a then r1 < r2 else r2 < r1 end;
 
 fun ord (Rat (false, _, _), Rat (true, _, _)) = LESS
   | ord (Rat (true, _, _), Rat (false, _, _)) = GREATER