fixed thm_less;
authorwenzelm
Thu Jan 08 18:19:48 1998 +0100 (1998-01-08)
changeset 45380f40d6e7897d
parent 4537 4e835bd9fada
child 4539 4227bd14dbe7
fixed thm_less;
src/Pure/Thy/thm_database.ML
     1.1 --- a/src/Pure/Thy/thm_database.ML	Thu Jan 08 18:10:34 1998 +0100
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Jan 08 18:19:48 1998 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4              end
     1.5  
     1.6        fun thm_less ((p0:int,s0:int,_),(p1,s1,_)) =
     1.7 -            (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
     1.8 +            (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<s1)
     1.9              orelse (p0=0 andalso p1<>0)
    1.10  
    1.11        fun select((p as (_,thm))::named_thms, sels) =