--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Aug 04 17:39:47 2024 +0200
@@ -198,10 +198,10 @@
val ctxt = Proof_Context.init_global thy
fun filtering th =
if is_equationlike th andalso
- defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
+ defining_const_of_equation (normalize_equation thy th) = dest_Const_name t then
SOME (normalize_equation thy th)
else
- if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
+ if is_introlike th andalso defining_const_of_introrule th = dest_Const_name t then
SOME th
else
NONE