fixed thm_less;
authorwenzelm
Thu, 08 Jan 1998 18:19:48 +0100
changeset 4538 0f40d6e7897d
parent 4537 4e835bd9fada
child 4539 4227bd14dbe7
fixed thm_less;
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) =