--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Aug 04 17:39:47 2024 +0200
@@ -785,7 +785,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees;
+ val co_rec_names = map (dest_Const_name o Morphism.term phi) co_rec_frees;
val co_recs = @{map 2} (fn name => fn resT =>
Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
val co_rec_defs = map (fn def =>