# 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'