src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

 Sugared datatype and codatatype constructions.
 *)
 
 signature BNF_FP_DEF_SUGAR =
 sig
-  val derive_induct_fold_rec_thms_for_types: int -> BNF_Def.BNF list -> thm -> thm list ->
-    thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
-    typ list list list -> int list list -> int list -> term list list -> term list list ->
-    term list list -> term list list list -> thm list list -> term list -> term list -> thm list ->
-    thm list -> Proof.context ->
+  val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
+    BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
+    int list list -> int list -> term list list -> term list list -> term list list -> term list
+    list list -> thm list list -> term list -> term list -> thm list -> thm list -> Proof.context ->
     (thm * thm list * Args.src list) * (thm list list * Args.src list)
       * (thm list list * Args.src list)
-  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context -> int ->
+  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context ->
     BNF_Def.BNF list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list ->
     BNF_Def.BNF list -> typ list -> typ list -> typ list -> int list list -> int list list ->
     int list -> term list -> term list list -> term list list -> term list list list list ->
     term list list list list -> term list list -> term list list list list ->
     term list list list list -> term list list -> thm list list ->

     val live = live_of_bnf bnf;
     val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
     val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
   in Term.list_comb (rel, map build_arg Ts') end;
 
-fun derive_induct_fold_rec_thms_for_types nn pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
+fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
     nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
     fold_defs rec_defs lthy =
   let
+    val nn = length pre_bnfs;
+
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;

   in
     ((induct_thm, induct_thms, [induct_case_names_attr]),
      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
   end;
 
-fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs dtor_coinduct
+fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy pre_bnfs dtor_coinduct
     dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
     As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
     unfolds corecs unfold_defs corec_defs lthy =
   let
+    val nn = length pre_bnfs;
+
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs;
     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;

           map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
               (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
             dtor_corec_thms pre_map_defs ctr_defss;
 
         fun prove goal tac =
-          Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
+          Goal.prove_sorry lthy [] [] goal (tac o #context)
+          |> Thm.close_derivation;
 
         val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
         val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
 
         val filter_safesss =

         (((ctrss, xsss, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =
       let
         val ((induct_thm, induct_thms, induct_attrs),
              (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
-          derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
+          derive_induct_fold_rec_thms_for_types pre_bnfs fp_induct fp_fold_thms fp_rec_thms
             nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
             fold_defs rec_defs lthy;
 
         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
 

              (unfold_thmss, corec_thmss, corec_like_attrs),
              (safe_unfold_thmss, safe_corec_thmss),
              (disc_unfold_thmss, disc_corec_thmss, disc_corec_like_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_corec_like_iff_attrs),
              (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
-          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
+          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy pre_bnfs fp_induct
             fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
             kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
             unfolds corecs unfold_defs corec_defs lthy;
 
         fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));