src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

     val ctr_binderss = map (map ctr_of) ctr_specss;
     val ctr_argsss = map (map args_of) ctr_specss;
     val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
 
     val sel_bindersss = map (map (map fst)) ctr_argsss;
-    val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
-
-    val rhs_As' = fold (fold (fold Term.add_tfreesT)) ctr_Tsss [];
+    val fake_ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
+
+    val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
     val _ = (case subtract (op =) As' rhs_As' of
         [] => ()
       | A' :: _ => error ("Extra type variables on rhs: " ^
           quote (Syntax.string_of_typ lthy (TFree A'))));
 

         (case find_index (is_same_recT T) fake_Ts of
           ~1 => Type (s, map freeze_recXs Us)
         | i => nth Xs i)
       | freeze_recXs T = T;
 
-    val ctr_TsssXs = map (map (map freeze_recXs)) ctr_Tsss;
+    val ctr_TsssXs = map (map (map freeze_recXs)) fake_ctr_Tsss;
     val sum_prod_TsXs = map (mk_sumTN o map HOLogic.mk_tupleT) ctr_TsssXs;
 
     val eqs = map dest_TFree Xs ~~ sum_prod_TsXs;
 
     val ((raw_unfs, raw_flds, raw_fp_iters, raw_fp_recs, unf_flds, fld_unfs, fld_injects), lthy') =

 
     val unfs = map (mk_unf As) raw_unfs;
     val flds = map (mk_fld As) raw_flds;
 
     val fp_Ts = map (domain_type o fastype_of) unfs;
+    val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fp_Ts)))) ctr_TsssXs;
 
     fun mk_fp_iter_or_rec Ts Us t =
       let
         val (binders, body) = strip_type (fastype_of t);
         val Type (_, Ts0) = if gfp then body else List.last binders;