# HG changeset patch
# User wenzelm
# Date 1683573061 -7200
# Node ID efc26a232a74d28efb47659fe07f52f590b538b9
# Parent  6413c598d21f30ee0572d5111551d7c98f67de3c
tuned;

diff -r 6413c598d21f -r efc26a232a74 src/Pure/Tools/find_theorems.ML
--- 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'