--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -1059,7 +1059,7 @@
let
val (bs, mxs) = map_split (apfst fst) fixes;
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
- val primcorec_types = map (#1 o dest_Type) res_Ts;
+ val primcorec_types = map dest_Type_name res_Ts;
val _ = check_duplicate_const_names bs;
val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts);