changeset 77995 | efc26a232a74 |
parent 77854 | 64533f3818a4 |
child 80328 | 559909bd7715 |
--- 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'