tuned;

--- a/src/Pure/Tools/find_theorems.ML	Mon May 08 11:45:58 2023 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon May 08 21:11:01 2023 +0200
@@ -236,7 +236,7 @@
     val thy = Proof_Context.theory_of ctxt;
     fun matches obj ctxt' = Pattern.matches thy (pat, obj) orelse
       (case obj of
-        Abs (_, T, t) =>
+        Abs _ =>
           let val ((_, t'), ctxt'') = Variable.dest_abs obj ctxt'
           in matches t' ctxt'' end
       | t $ u => matches t ctxt' orelse matches u ctxt'