--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Mar 27 12:08:08 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Mar 27 14:47:49 2019 +0100
@@ -1059,6 +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 _ = check_duplicate_const_names bs;
val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts);
@@ -1532,7 +1533,7 @@
val fun_ts0 = map fst def_infos;
in
lthy
- |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat sel_thmss)
+ |> Spec_Rules.add (Spec_Rules.equational_primcorec primcorec_types) (fun_ts0, flat sel_thmss)
|> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat ctr_thmss)
|> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat code_thmss)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))