src/Pure/Tools/find_theorems.ML

   in betapplys (t, ts) end;
 
 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
+fun matches_subterm ctxt (pat, obj) =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    fun matches obj ctxt' = Pattern.matches thy (pat, obj) orelse
       (case obj of
-        Abs (_, 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;
+        Abs (_, T, t) =>
+          let val ((_, t'), ctxt'') = Variable.dest_abs obj ctxt'
+          in matches t' ctxt'' end
+      | t $ u => matches t ctxt' orelse matches u ctxt'
+      | _ => false);
+  in matches obj ctxt 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

     val pat' = (expand_abs o Envir.eta_contract) pat;
     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
-            matches_subterm (Proof_Context.theory_of ctxt) (pat', Thm.full_prop_of thm)
+            matches_subterm 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 *)