src/Pure/Tools/find_theorems.ML

 
 (* filter_pattern *)
 
 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
 
+(* Does pat match a subterm of obj? *)
+fun matches_subterm thy (pat, obj) =
+  let
+    fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
+      (case obj of
+        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
+      | t $ u => msub bounds t orelse msub bounds u
+      | _ => false)
+  in msub 0 obj end;
+
 (*Including all constants and frees is only sound because matching
   uses higher-order patterns. If full matching were used, then
   constants that may be subject to beta-reduction after substitution
   of frees should not be included for LHS set because they could be
   thrown away by the substituted function.  E.g. for (?F 1 2) do not

     val pat_consts = get_names pat;
 
     fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
       | check ((_, thm), c as SOME thm_consts) =
          (if subset (op =) (pat_consts, thm_consts) andalso
-            Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
+            matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
           then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
   in check end;
 
 
 (* interpret criteria as filters *)