--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 12:06:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 12:43:34 2012 +0200
@@ -977,10 +977,9 @@
val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
- val (((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
+ val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
(iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
- |> mk_Frees "z" Ts
- ||>> mk_Frees' "z1" Ts
+ |> mk_Frees' "z1" Ts
||>> mk_Frees' "z2" Ts'
||>> mk_Frees' "x" FTs
||>> mk_Frees "y" FTs'
@@ -989,6 +988,7 @@
||>> mk_Frees "f" fTs
||>> mk_Frees "s" rec_sTs;
+ val Izs = map2 retype_free Ts zs;
val phis = map2 retype_free (map mk_predT Ts) init_phis;
val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis;