# HG changeset patch
# User wenzelm
# Date 884279988 -3600
# Node ID 0f40d6e7897d49868456010ea2781f784f2a51c5
# Parent  4e835bd9fada8dc70846cf7cab8cd70d9ee68587
fixed thm_less;

diff -r 4e835bd9fada -r 0f40d6e7897d src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Jan 08 18:10:34 1998 +0100
+++ b/src/Pure/Thy/thm_database.ML	Thu Jan 08 18:19:48 1998 +0100
@@ -134,7 +134,7 @@
             end
 
       fun thm_less ((p0:int,s0:int,_),(p1,s1,_)) =
-            (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
+            (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<s1)
             orelse (p0=0 andalso p1<>0)
 
       fun select((p as (_,thm))::named_thms, sels) =