careful about constructor types w.r.t. fake context (third step of localization)
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 06 12:04:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 06 12:14:40 2012 +0200
@@ -87,9 +87,9 @@
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 fake_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 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: " ^
@@ -112,7 +112,7 @@
| 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;
@@ -134,6 +134,7 @@
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