src/Pure/Thy/thm_database.ML

--- a/src/Pure/Thy/thm_database.ML	Fri Dec 19 09:57:24 1997 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Dec 19 09:58:03 1997 +0100
@@ -133,7 +133,7 @@
 		(0, map (fn (_,t) => size_of_term t) subst)
             end
 
-      fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
+      fun thm_less ((p0:int,s0:int,_),(p1,s1,_)) =
             (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
             orelse (p0=0 andalso p1<>0)
 
@@ -148,7 +148,7 @@
             end
         | select([],sels) = sels
 
-  in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
+  in map (fn (_,_,t) => t) (sort (make_ord thm_less) (select(named_thms, []))) end; 
 
 fun find_matching(prop,sign,index,extract) =
   (case top_const prop of