# HG changeset patch
# User blanchet
# Date 1347446614 -7200
# Node ID f4169aa675130f4b53aa4fbfcf063c3afd78f8c1
# Parent  276ff43ee0b19156133c98446a9ca0777f9fcd5a
free variable name tuning

diff -r 276ff43ee0b1 -r f4169aa67513 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- 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;