# HG changeset patch
# User berghofe
# Date 829044747 -7200
# Node ID faa643c33ee61c0bd3aff13458512a46e8970200
# Parent  1a2ffa2fbf7d84b21dcb95d9e817a8cef8967708
select_match now sorts list of matching theorems according to the
number of premises and size of the required substitution

diff -r 1a2ffa2fbf7d -r faa643c33ee6 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Apr 04 20:13:46 1996 +0200
+++ b/src/Pure/Thy/thm_database.ML	Tue Apr 09 12:12:27 1996 +0200
@@ -198,16 +198,27 @@
               None => false
             | Some pat => Pattern.matches tsig (pat, obj);
 
+      fun substsize(prop, tsig) =
+            let val Some pat = extract prop
+                val (_,subst) = Pattern.match tsig (pat,obj)
+            in sum(map (fn (_,t) => size_of_term t) subst) end
+
+      fun thm_order ((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)
+
       fun select((p as (_,thm))::named_thms, sels) =
             let val {prop, sign, ...} = rep_thm thm
             in select(named_thms,
                       if Sign.subsig(sign, signobj) andalso
                          matches(prop,#tsig(Sign.rep_sg signobj))
-                      then p::sels else sels)
+                      then
+			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
+                      else sels)
             end
         | select([],sels) = sels
 
-  in select(named_thms, []) end;
+  in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
 
 fun find_matching(prop,sign,index,extract) =
   (case top_const prop of