src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

     in
       t' |> fold_rev absfree abstractions
     end
   else Const (@{const_name undefined}, dummyT)
 
-fun build_defs lthy bs funs_data rec_specs get_indices =
+fun build_defs lthy bs mxs funs_data rec_specs get_indices =
   let
     val n_funs = length funs_data;
 
     val ctr_spec_eqn_data_list' =
       (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data

         hd x |> #left_args |> length) funs_data;
   in
     (recs, ctr_poss)
     |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
     |> Syntax.check_terms lthy
-    |> map2 (fn b => fn t => ((b, NoSyn), ((Binding.map_name Thm.def_name b, []), t))) bs
+    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
   end;
 
 fun find_rec_calls get_indices eqn_data =
   let
     fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg

     |> (fn [] => NONE | callss => SOME (#ctr eqn_data, callss))
   end;
 
 fun add_primrec fixes specs lthy =
   let
-    val bs = map (fst o fst) fixes;
+    val (bs, mxs) = map_split (apfst fst) fixes;
     val fun_names = map Binding.name_of bs;
     val eqns_data = map (snd #> dissect_eqn lthy fun_names) specs;
     val funs_data = eqns_data
       |> partition_eq ((op =) o pairself #fun_name)
       |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst

     val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
       map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
         primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^
           " is not a constructor in left-hand side") user_eqn) eqns_data end;
 
-    val defs = build_defs lthy' bs funs_data rec_specs get_indices;
+    val defs = build_defs lthy' bs mxs funs_data rec_specs get_indices;
 
     fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
         lthy =
       let
         val fun_name = #fun_name (hd fun_data);

       in
         abs_args o update_args
       end
   end;
 
-fun co_build_defs lthy sequential bs arg_Tss fun_name_corec_spec_list eqns_data =
+fun co_build_defs lthy sequential bs mxs arg_Tss fun_name_corec_spec_list eqns_data =
   let
     val fun_names = map Binding.name_of bs;
 
     val disc_eqnss = map_filter (try (fn Disc x => x)) eqns_data
       |> partition_eq ((op =) o pairself #fun_name)

   in
     map (list_comb o rpair corec_args) corecs
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy
-    |> map2 (fn b => fn t => ((b, NoSyn), ((Binding.map_name Thm.def_name b, []), t))) bs
+    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
     |> rpair proof_obligations
   end;
 
 fun add_primcorec sequential fixes specs lthy =
   let
-    val bs = map (fst o fst) fixes;
+    val (bs, mxs) = map_split (apfst fst) fixes;
     val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
 
     (* copied from primrec_new *)
     fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes
       |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)

     val (eqns_data, _) =
       fold_map (co_dissect_eqn sequential fun_name_corec_spec_list) (map snd specs) []
       |>> flat;
 
     val (defs, proof_obligations) =
-      co_build_defs lthy' sequential bs (map (binder_types o snd o fst) fixes)
+      co_build_defs lthy' sequential bs mxs (map (binder_types o snd o fst) fixes)
         fun_name_corec_spec_list eqns_data;
   in
     lthy'
     |> fold_map Local_Theory.define defs |> snd
     |> Proof.theorem NONE (K I) [map (rpair []) proof_obligations]