# HG changeset patch
# User blanchet
# Date 1410210563 -7200
# Node ID ff8059e3e803f8b84f631b7c810aa7eb007b4bbe
# Parent  b05ed697708eda98c25bb5de5446270f3ce19c25
generate better internal names, with name of the target type in it

diff -r b05ed697708e -r ff8059e3e803 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Sep 08 23:09:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Sep 08 23:09:23 2014 +0200
@@ -70,15 +70,14 @@
     val b_names = map Binding.name_of bs;
     val b_name = mk_common_name b_names;
     val b = Binding.name b_name;
-    val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
-    fun mk_internal_bs name =
-      map (fn b =>
-        Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
+
+    fun mk_internal_of_b name =
+      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
+    fun mk_internal_b name = mk_internal_of_b name b;
+    fun mk_internal_bs name = map (mk_internal_of_b name) bs;
     val external_bs = map2 (Binding.prefix false) b_names bs
       |> not note_all ? map Binding.conceal;
 
-    (* 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);
diff -r b05ed697708e -r ff8059e3e803 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 08 23:09:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 08 23:09:23 2014 +0200
@@ -40,15 +40,14 @@
     val b_names = map Binding.name_of bs;
     val b_name = mk_common_name b_names;
     val b = Binding.name b_name;
-    val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
-    fun mk_internal_bs name =
-      map (fn b =>
-        Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
+
+    fun mk_internal_of_b name =
+      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
+    fun mk_internal_b name = mk_internal_of_b name b;
+    fun mk_internal_bs name = map (mk_internal_of_b name) bs;
     val external_bs = map2 (Binding.prefix false) b_names bs
       |> not note_all ? map Binding.conceal;
 
-    (* 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);