1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 18 19:57:59 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 18 20:43:55 2013 +0200
     1.3 @@ -31,6 +31,8 @@
     1.4       sels: term list,
     1.5       pred: int option,
     1.6       calls: corec_call list,
     1.7 +     discI: thm,
     1.8 +     sel_thms: thm list,
     1.9       collapse: thm,
    1.10       corec_thm: thm,
    1.11       disc_corec: thm,
    1.12 @@ -96,6 +98,8 @@
    1.13     sels: term list,
    1.14     pred: int option,
    1.15     calls: corec_call list,
    1.16 +   discI: thm,
    1.17 +   sel_thms: thm list,
    1.18     collapse: thm,
    1.19     corec_thm: thm,
    1.20     disc_corec: thm,
    1.21 @@ -431,11 +435,13 @@
    1.22           else No_Corec) g_i
    1.23        | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
    1.24  
    1.25 -    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
    1.26 +    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
    1.27 +        disc_corec sel_corecs =
    1.28        let val nullary = not (can dest_funT (fastype_of ctr)) in
    1.29          {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
    1.30 -         calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
    1.31 -         corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs}
    1.32 +         calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
    1.33 +         collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
    1.34 +         sel_corecs = sel_corecs}
    1.35        end;
    1.36  
    1.37      fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
    1.38 @@ -445,14 +451,16 @@
    1.39          val discs = #discs (nth ctr_sugars index);
    1.40          val selss = #selss (nth ctr_sugars index);
    1.41          val p_ios = map SOME p_is @ [NONE];
    1.42 +        val discIs = #discIs (nth ctr_sugars index);
    1.43 +        val sel_thmss = #sel_thmss (nth ctr_sugars index);
    1.44          val collapses = #collapses (nth ctr_sugars index);
    1.45          val corec_thms = co_rec_of (nth coiter_thmsss index);
    1.46          val disc_corecs = (case co_rec_of (nth disc_coitersss index) of [] => [TrueI]
    1.47            | thms => thms);
    1.48          val sel_corecss = co_rec_of (nth sel_coiterssss index);
    1.49        in
    1.50 -        map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
    1.51 -          disc_corecs sel_corecss
    1.52 +        map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
    1.53 +          corec_thms disc_corecs sel_corecss
    1.54        end;
    1.55  
    1.56      fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,

     2.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 18 19:57:59 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 18 20:43:55 2013 +0200
     2.3 @@ -29,6 +29,9 @@
     2.4    val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) ->
     2.5      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     2.6      'i list -> 'j list -> 'k list -> 'l list -> 'm list
     2.7 +  val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
     2.8 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     2.9 +    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
    2.10    val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
    2.11    val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
    2.12      'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
    2.13 @@ -248,6 +251,13 @@
    2.14        map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
    2.15    | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    2.16  
    2.17 +fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
    2.18 +  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
    2.19 +      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
    2.20 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
    2.21 +      map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
    2.22 +  | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    2.23 +
    2.24  fun fold_map2 _ [] [] acc = ([], acc)
    2.25    | fold_map2 f (x1::x1s) (x2::x2s) acc =
    2.26      let