author berghofe Tue, 09 Apr 1996 12:12:27 +0200 changeset 1654 faa643c33ee6 parent 1653 1a2ffa2fbf7d child 1655 5be64540f275
select_match now sorts list of matching theorems according to the number of premises and size of the required substitution
```--- 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```