src/HOL/Codatatype/Tools/bnf_lfp.ML
changeset 49331 f4169aa67513
parent 49330 276ff43ee0b1
child 49337 538687a77075
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 12:06:03 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 12:43:34 2012 +0200
     1.3 @@ -977,10 +977,9 @@
     1.4      val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
     1.5      val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
     1.6  
     1.7 -    val (((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
     1.8 +    val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
     1.9        (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
    1.10 -      |> mk_Frees "z" Ts
    1.11 -      ||>> mk_Frees' "z1" Ts
    1.12 +      |> mk_Frees' "z1" Ts
    1.13        ||>> mk_Frees' "z2" Ts'
    1.14        ||>> mk_Frees' "x" FTs
    1.15        ||>> mk_Frees "y" FTs'
    1.16 @@ -989,6 +988,7 @@
    1.17        ||>> mk_Frees "f" fTs
    1.18        ||>> mk_Frees "s" rec_sTs;
    1.19  
    1.20 +    val Izs = map2 retype_free Ts zs;
    1.21      val phis = map2 retype_free (map mk_predT Ts) init_phis;
    1.22      val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis;
    1.23