diff -r ae8c9380bbc4 -r 43a1cc050943 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Aug 31 22:32:43 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Aug 31 23:49:14 2013 +0200
@@ -253,7 +253,7 @@
     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;
 
@@ -282,7 +282,7 @@
     (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 =
@@ -311,7 +311,7 @@
 
 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
@@ -340,7 +340,7 @@
         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 =
@@ -638,7 +638,7 @@
       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;
 
@@ -692,13 +692,13 @@
     |> 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 *)
@@ -723,7 +723,7 @@
       |>> 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'