--- a/src/Pure/Thy/thm_database.ML Fri Jul 17 10:50:01 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML Fri Jul 17 10:50:28 1998 +0200
@@ -120,6 +120,9 @@
val As = Logic.strip_assums_hyp gi
in map (fn A => subst_bounds(frees,A)) As end;
+(*returns all those named_thms whose subterm extracted by extract can be
+ instantiated to obj; the list is sorted according to the number of premises
+ and the size of the required substitution.*)
fun select_match(obj, signobj, named_thms, extract) =
let fun matches(prop, tsig) =
case extract prop of