src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49330 276ff43ee0b1
parent 49327 541d818d2ff3
child 49337 538687a77075
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 11:47:51 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 12:06:03 2012 +0200
     1.3 @@ -1873,7 +1873,7 @@
     1.4        ||>> mk_Frees "f" coiter_fTs
     1.5        ||>> mk_Frees "g" coiter_fTs
     1.6        ||>> mk_Frees "s" corec_sTs
     1.7 -      ||>> mk_Frees "phi" (map (fn T => T --> T --> HOLogic.boolT) Ts);
     1.8 +      ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts);
     1.9  
    1.10      fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
    1.11      val unf_name = Binding.name_of o unf_bind;
    1.12 @@ -2291,7 +2291,7 @@
    1.13          val pTs = map2 (curry op -->) passiveXs passiveCs;
    1.14          val uTs = map2 (curry op -->) Ts Ts';
    1.15          val JRTs = map2 (curry mk_relT) passiveAs passiveBs;
    1.16 -        val JphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
    1.17 +        val JphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
    1.18          val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts';
    1.19          val B1Ts = map HOLogic.mk_setT passiveAs;
    1.20          val B2Ts = map HOLogic.mk_setT passiveBs;
    1.21 @@ -2309,7 +2309,7 @@
    1.22            ||>> mk_Frees "u" uTs
    1.23            ||>> mk_Frees' "b" Ts'
    1.24            ||>> mk_Frees' "b" Ts'
    1.25 -          ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> U --> HOLogic.boolT) Ts) passiveAs)
    1.26 +          ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
    1.27            ||>> mk_Frees "R" JRTs
    1.28            ||>> mk_Frees "phi" JphiTs
    1.29            ||>> mk_Frees "B1" B1Ts