# HG changeset patch
# User blanchet
# Date 1347444363 -7200
# Node ID 276ff43ee0b19156133c98446a9ca0777f9fcd5a
# Parent  82452dc63ed55384a57066cb09d2d2999075a56e
reuse generated names (they look better + slightly more efficient)

diff -r 82452dc63ed5 -r 276ff43ee0b1 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:47:51 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 12:06:03 2012 +0200
@@ -59,12 +59,8 @@
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
-fun retype_free T (Free (s, _)) = Free (s, T);
-
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
-fun mk_predT T = T --> HOLogic.boolT;
-
 fun mk_id T = Const (@{const_name id}, T --> T);
 
 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
diff -r 82452dc63ed5 -r 276ff43ee0b1 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 11:47:51 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 12:06:03 2012 +0200
@@ -83,6 +83,10 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
+  val retype_free: typ -> term -> term
+
+  val mk_predT: typ -> typ;
+
   val mk_sumTN: typ list -> typ
   val mk_sumTN_balanced: typ list -> typ
 
@@ -211,6 +215,10 @@
 
 val mk_bundle_name = space_implode "_" o map Binding.name_of;
 
+fun mk_predT T = T --> HOLogic.boolT;
+
+fun retype_free T (Free (s, _)) = Free (s, T);
+
 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
 
 fun dest_sumTN 1 T = [T]
diff -r 82452dc63ed5 -r 276ff43ee0b1 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 11:47:51 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 12:06:03 2012 +0200
@@ -1873,7 +1873,7 @@
       ||>> mk_Frees "f" coiter_fTs
       ||>> mk_Frees "g" coiter_fTs
       ||>> mk_Frees "s" corec_sTs
-      ||>> mk_Frees "phi" (map (fn T => T --> T --> HOLogic.boolT) Ts);
+      ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts);
 
     fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
     val unf_name = Binding.name_of o unf_bind;
@@ -2291,7 +2291,7 @@
         val pTs = map2 (curry op -->) passiveXs passiveCs;
         val uTs = map2 (curry op -->) Ts Ts';
         val JRTs = map2 (curry mk_relT) passiveAs passiveBs;
-        val JphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
+        val JphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
         val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts';
         val B1Ts = map HOLogic.mk_setT passiveAs;
         val B2Ts = map HOLogic.mk_setT passiveBs;
@@ -2309,7 +2309,7 @@
           ||>> mk_Frees "u" uTs
           ||>> mk_Frees' "b" Ts'
           ||>> mk_Frees' "b" Ts'
-          ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> U --> HOLogic.boolT) Ts) passiveAs)
+          ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
           ||>> mk_Frees "R" JRTs
           ||>> mk_Frees "phi" JphiTs
           ||>> mk_Frees "B1" B1Ts
diff -r 82452dc63ed5 -r 276ff43ee0b1 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 11:47:51 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 12:06:03 2012 +0200
@@ -792,7 +792,7 @@
       ||>> mk_Frees' "x" init_FTs
       ||>> mk_Frees "f" init_fTs
       ||>> mk_Frees "f" init_fTs
-      ||>> mk_Frees "phi" (replicate n (initT --> HOLogic.boolT));
+      ||>> mk_Frees "phi" (replicate n (mk_predT initT));
 
     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
       (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
@@ -977,8 +977,8 @@
     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')),
-      (iter_f, iter_f')), fs), phis), phi2s), rec_ss), names_lthy) = names_lthy
+    val (((((((((Izs, (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' "z2" Ts'
@@ -987,10 +987,11 @@
       ||>> mk_Freess' "z" setFTss
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
       ||>> mk_Frees "f" fTs
-      ||>> mk_Frees "phi" (map (fn T => T --> HOLogic.boolT) Ts)
-      ||>> mk_Frees "phi" (map2 (fn T => fn U => T --> U --> HOLogic.boolT) Ts Ts')
       ||>> mk_Frees "s" rec_sTs;
 
+    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;
+
     fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1));
     val fld_name = Binding.name_of o fld_bind;
     val fld_def_bind = rpair [] o Thm.def_binding o fld_bind;
@@ -1353,7 +1354,7 @@
         val XTs = mk_Ts passiveXs;
         val YTs = mk_Ts passiveYs;
         val IRTs = map2 (curry mk_relT) passiveAs passiveBs;
-        val IphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
+        val IphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
 
         val (((((((((((((((fs, fs'), fs_copy), us),
           B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),