1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4      val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
     1.5        else ();
     1.6  
     1.7 -    val N = length specs;
     1.8 +    val nn = length specs;
     1.9      val fp_bs = map type_binding_of specs;
    1.10      val fp_common_name = mk_common_name fp_bs;
    1.11  
    1.12 @@ -107,8 +107,8 @@
    1.13      val (((Bs, Cs), vs'), no_defs_lthy) =
    1.14        no_defs_lthy0
    1.15        |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
    1.16 -      |> mk_TFrees N
    1.17 -      ||>> mk_TFrees N
    1.18 +      |> mk_TFrees nn
    1.19 +      ||>> mk_TFrees nn
    1.20        ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
    1.21  
    1.22      (* TODO: cleaner handling of fake contexts, without "background_theory" *)
    1.23 @@ -568,7 +568,8 @@
    1.24                | mk_prem_prems _ _ = [];
    1.25  
    1.26              fun close_prem_prem (Free x') t =
    1.27 -              fold_rev Logic.all (map Free (drop (N + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.28 +              fold_rev Logic.all
    1.29 +                (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.30  
    1.31              fun mk_prem phi ctr ctr_Ts =
    1.32                let
    1.33 @@ -591,7 +592,7 @@
    1.34                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.35                  mk_induct_tac ctxt);
    1.36            in
    1.37 -            `(conj_dests N) induct_thm
    1.38 +            `(conj_dests nn) induct_thm
    1.39            end;
    1.40  
    1.41          val (iter_thmss, rec_thmss) =
    1.42 @@ -643,7 +644,7 @@
    1.43            end;
    1.44  
    1.45          val common_notes =
    1.46 -          (if N > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
    1.47 +          (if nn > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
    1.48            |> map (fn (thmN, thms, attrs) =>
    1.49                ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.50  
    1.51 @@ -666,7 +667,7 @@
    1.52            let
    1.53              val coinduct_thm = fp_induct;
    1.54            in
    1.55 -            `(conj_dests N) coinduct_thm
    1.56 +            `(conj_dests nn) coinduct_thm
    1.57            end;
    1.58  
    1.59          val (coiter_thmss, corec_thmss) =
    1.60 @@ -749,7 +750,7 @@
    1.61            map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
    1.62  
    1.63          val common_notes =
    1.64 -          (if N > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
    1.65 +          (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
    1.66            |> map (fn (thmN, thms, attrs) =>
    1.67                ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.68