# HG changeset patch
# User blanchet
# Date 1376256957 -7200
# Node ID 1b62f05ab4fd1c76a9838835de4e1f68a9e37de6
# Parent  797362ce0c144c04e8009ffbd049fa73ebf2735b
honor user tfree names

diff -r 797362ce0c14 -r 1b62f05ab4fd src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sat Aug 10 12:00:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Aug 11 23:35:57 2013 +0200
@@ -62,21 +62,23 @@
     val live = live_of_bnf (hd bnfs);
     val n = length bnfs; (*active*)
     val ks = 1 upto n;
-    val m = live - n (*passive, if 0 don't generate a new BNF*);
+    val m = live - n; (*passive, if 0 don't generate a new BNF*)
     val ls = 1 upto m;
-    val b = Binding.name (mk_common_name (map Binding.name_of bs));
+    val b_names = map Binding.name_of bs;
+    val b = Binding.name (mk_common_name b_names);
 
     (* TODO: check if m, n, etc., are sane *)
 
     val deads = fold (union (op =)) Dss resDs;
     val names_lthy = fold Variable.declare_typ deads lthy;
+    val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
 
     (* tvars *)
     val ((((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), passiveXs),
         passiveYs), idxT) = names_lthy
-      |> mk_TFrees m
+      |> variant_tfrees passives
       ||>> mk_TFrees n
-      ||>> mk_TFrees m
+      ||>> variant_tfrees passives
       ||>> mk_TFrees n
       ||>> mk_TFrees m
       ||>> mk_TFrees n
@@ -96,7 +98,7 @@
 
     (* types *)
     val dead_poss =
-      map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs;
+      map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs;
     fun mk_param NONE passive = (hd passive, tl passive)
       | mk_param (SOME a) passive = (a, passive);
     val mk_params = fold_map mk_param dead_poss #> fst;
@@ -232,7 +234,7 @@
 
     (* derived thms *)
 
-    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x)=
+    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
       map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
     fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
       let
diff -r 797362ce0c14 -r 1b62f05ab4fd src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sat Aug 10 12:00:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Aug 11 23:35:57 2013 +0200
@@ -34,19 +34,21 @@
     val n = length bnfs; (*active*)
     val ks = 1 upto n;
     val m = live - n; (*passive, if 0 don't generate a new BNF*)
-    val b = Binding.name (mk_common_name (map Binding.name_of bs));
+    val b_names = map Binding.name_of bs;
+    val b = Binding.name (mk_common_name b_names);
 
     (* TODO: check if m, n, etc., are sane *)
 
     val deads = fold (union (op =)) Dss resDs;
     val names_lthy = fold Variable.declare_typ deads lthy;
+    val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
 
     (* tvars *)
     val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) =
       names_lthy
-      |> mk_TFrees m
+      |> variant_tfrees passives
       ||>> mk_TFrees n
-      ||>> mk_TFrees m
+      ||>> variant_tfrees passives
       ||>> mk_TFrees n
       ||>> mk_TFrees n
       ||>> mk_TFrees m
@@ -63,7 +65,7 @@
 
     (* types *)
     val dead_poss =
-      map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs;
+      map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs;
     fun mk_param NONE passive = (hd passive, tl passive)
       | mk_param (SOME a) passive = (a, passive);
     val mk_params = fold_map mk_param dead_poss #> fst;
@@ -189,7 +191,7 @@
 
     (* derived thms *)
 
-    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x)=
+    (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
       map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
     fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
       let