1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 17:59:41 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 11 18:13:17 2013 +0100
     1.3 @@ -134,9 +134,9 @@
     1.4  
     1.5      val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
     1.6      val mapss = map (of_fp_sugar #mapss) fp_sugars0;
     1.7 -    val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
     1.8 +    val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
     1.9  
    1.10 -    val ctrss = map #ctrs ctr_sugars0;
    1.11 +    val ctrss = map #ctrs ctr_sugars;
    1.12      val ctr_Tss = map (map fastype_of) ctrss;
    1.13  
    1.14      val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
    1.15 @@ -214,13 +214,6 @@
    1.16                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
    1.17            |>> split_list;
    1.18  
    1.19 -        val rho = tvar_subst thy ctr_Ts fpTs;
    1.20 -        val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
    1.21 -            (Morphism.term_morphism (Term.subst_TVars rho));
    1.22 -        val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
    1.23 -
    1.24 -        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
    1.25 -
    1.26          val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
    1.27                sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
    1.28            if fp = Least_FP then