src/Pure/Thy/thm_database.ML

 fun prems_of_goal i =
   let val (gi,frees) = goal_params i
       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
               None => false
             | Some pat => Pattern.matches tsig (pat, obj);