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