# HG changeset patch
# User blanchet
# Date 1376055638 -7200
# Node ID 3b3e52d5e66b6e688c776766035df890de8a1a57
# Parent  cdd1d50492873a26c78abbeeca54eb2788e0906a
tuned name generation code (to make it easier to adapt later)

diff -r cdd1d5049287 -r 3b3e52d5e66b src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Aug 09 15:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Aug 09 15:40:38 2013 +0200
@@ -72,19 +72,21 @@
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
-    val ((((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
-      (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy
-      |> mk_TFrees live
-      |> apfst (`(chop m))
-      ||> mk_TFrees live
-      ||>> apfst (`(chop m))
-      ||> mk_TFrees live
-      ||>> apfst (chop m)
+    val ((((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), passiveXs),
+        passiveYs), idxT) = names_lthy
+      |> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
       ||>> mk_TFrees m
       ||>> mk_TFrees m
       ||> fst o mk_TFrees 1
       ||> the_single;
 
+    val allAs = passiveAs @ activeAs;
+    val allBs' = passiveBs @ activeBs;
     val Ass = replicate n allAs;
     val allBs = passiveAs @ activeBs;
     val Bss = replicate n allBs;
diff -r cdd1d5049287 -r 3b3e52d5e66b src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Aug 09 15:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Aug 09 15:40:38 2013 +0200
@@ -42,16 +42,18 @@
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
-    val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
-      activeCs), passiveXs), passiveYs) = names_lthy
-      |> mk_TFrees live
-      |> apfst (`(chop m))
-      ||> mk_TFrees live
-      ||>> apfst (`(chop m))
+    val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) =
+      names_lthy
+      |> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
       ||>> mk_TFrees n
       ||>> mk_TFrees m
       ||> fst o mk_TFrees m;
 
+    val allAs = passiveAs @ activeAs;
+    val allBs' = passiveBs @ activeBs;
     val Ass = replicate n allAs;
     val allBs = passiveAs @ activeBs;
     val Bss = replicate n allBs;