src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

     (* TODO: sanity checks on arguments *)
 
     val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
       else ();
 
-    val N = length specs;
+    val nn = length specs;
     val fp_bs = map type_binding_of specs;
     val fp_common_name = mk_common_name fp_bs;
 
     fun prepare_type_arg (ty, c) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in

     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
 
     val (((Bs, Cs), vs'), no_defs_lthy) =
       no_defs_lthy0
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
-      |> mk_TFrees N
-      ||>> mk_TFrees N
+      |> mk_TFrees nn
+      ||>> mk_TFrees nn
       ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
 
     (* TODO: cleaner handling of fake contexts, without "background_theory" *)
     (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
       locale and shadows an existing global type*)

                     end)
                 | i => [HOLogic.mk_Trueprop (nth phis i $ x)])
               | mk_prem_prems _ _ = [];
 
             fun close_prem_prem (Free x') t =
-              fold_rev Logic.all (map Free (drop (N + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
+              fold_rev Logic.all
+                (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
 
             fun mk_prem phi ctr ctr_Ts =
               let
                 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
                 val prem_prems =

 
             val induct_thm =
               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
                 mk_induct_tac ctxt);
           in
-            `(conj_dests N) induct_thm
+            `(conj_dests nn) induct_thm
           end;
 
         val (iter_thmss, rec_thmss) =
           let
             val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;

              map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_recss rec_tacss)
           end;
 
         val common_notes =
-          (if N > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
+          (if nn > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
           |> map (fn (thmN, thms, attrs) =>
               ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes =
           [(inductN, map single induct_thms, []), (* FIXME: attribs *)

       let
         val (coinduct_thms, coinduct_thm) =
           let
             val coinduct_thm = fp_induct;
           in
-            `(conj_dests N) coinduct_thm
+            `(conj_dests nn) coinduct_thm
           end;
 
         val (coiter_thmss, corec_thmss) =
           let
             val z = the_single zs;

           map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
         val sel_corec_thmsss =
           map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
 
         val common_notes =
-          (if N > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
+          (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
           |> map (fn (thmN, thms, attrs) =>
               ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes =
           [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)