src/HOL/Codatatype/Tools/bnf_lfp.ML
changeset 49330 276ff43ee0b1
parent 49327 541d818d2ff3
child 49331 f4169aa67513
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 11:47:51 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 12:06:03 2012 +0200
     1.3 @@ -792,7 +792,7 @@
     1.4        ||>> mk_Frees' "x" init_FTs
     1.5        ||>> mk_Frees "f" init_fTs
     1.6        ||>> mk_Frees "f" init_fTs
     1.7 -      ||>> mk_Frees "phi" (replicate n (initT --> HOLogic.boolT));
     1.8 +      ||>> mk_Frees "phi" (replicate n (mk_predT initT));
     1.9  
    1.10      val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
    1.11        (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
    1.12 @@ -977,8 +977,8 @@
    1.13      val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
    1.14      val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
    1.15  
    1.16 -    val (((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
    1.17 -      (iter_f, iter_f')), fs), phis), phi2s), rec_ss), names_lthy) = names_lthy
    1.18 +    val (((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
    1.19 +      (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
    1.20        |> mk_Frees "z" Ts
    1.21        ||>> mk_Frees' "z1" Ts
    1.22        ||>> mk_Frees' "z2" Ts'
    1.23 @@ -987,10 +987,11 @@
    1.24        ||>> mk_Freess' "z" setFTss
    1.25        ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
    1.26        ||>> mk_Frees "f" fTs
    1.27 -      ||>> mk_Frees "phi" (map (fn T => T --> HOLogic.boolT) Ts)
    1.28 -      ||>> mk_Frees "phi" (map2 (fn T => fn U => T --> U --> HOLogic.boolT) Ts Ts')
    1.29        ||>> mk_Frees "s" rec_sTs;
    1.30  
    1.31 +    val phis = map2 retype_free (map mk_predT Ts) init_phis;
    1.32 +    val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis;
    1.33 +
    1.34      fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1));
    1.35      val fld_name = Binding.name_of o fld_bind;
    1.36      val fld_def_bind = rpair [] o Thm.def_binding o fld_bind;
    1.37 @@ -1353,7 +1354,7 @@
    1.38          val XTs = mk_Ts passiveXs;
    1.39          val YTs = mk_Ts passiveYs;
    1.40          val IRTs = map2 (curry mk_relT) passiveAs passiveBs;
    1.41 -        val IphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
    1.42 +        val IphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
    1.43  
    1.44          val (((((((((((((((fs, fs'), fs_copy), us),
    1.45            B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),