# HG changeset patch
# User blanchet
# Date 1376291322 -7200
# Node ID 96754402c85155ca87b394a56b2f464865fd89f4
# Parent  6a7ee03902c38a73d7a577cdf3854d6f467c218a
reverted ill-advised naming scheme of 5a77edcdbe54

diff -r 6a7ee03902c3 -r 96754402c851 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sun Aug 11 23:35:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Aug 12 09:08:42 2013 +0200
@@ -204,7 +204,7 @@
 
     val (As, B) =
       no_defs_lthy
-      |> variant_tfrees (map base_name_of_typ As0)
+      |> variant_tfrees (map (fst o fst o dest_TVar) As0)
       ||> the_single o fst o mk_TFrees 1;
 
     val dataT = Type (dataT_name, As);
diff -r 6a7ee03902c3 -r 96754402c851 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Sun Aug 11 23:35:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Aug 12 09:08:42 2013 +0200
@@ -131,6 +131,7 @@
 
   val co_prefix: fp_kind -> string
 
+  val base_name_of_typ: typ -> string
   val mk_common_name: string list -> string
 
   val split_conj_thm: thm -> thm list
@@ -348,6 +349,12 @@
 
 fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
 
+fun add_components_of_typ (Type (s, Ts)) =
+    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
+  | add_components_of_typ _ = I;
+
+fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
+
 val mk_common_name = space_implode "_";
 
 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
diff -r 6a7ee03902c3 -r 96754402c851 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Sun Aug 11 23:35:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Mon Aug 12 09:08:42 2013 +0200
@@ -71,8 +71,6 @@
   val variant_types: string list -> sort list -> Proof.context ->
     (string * sort) list * Proof.context
   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
-  val base_name_of_typ: typ -> string
-
   val nonzero_string_of_int: int -> string
 
   val num_binder_types: typ -> int
@@ -402,14 +400,6 @@
   apfst (map TFree) o
     variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
 
-fun add_components_of_typ (Type (s, Ts)) =
-    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
-  | add_components_of_typ (TFree (s, _)) = cons s
-  | add_components_of_typ (TVar ((s, _), _)) = cons s
-  | add_components_of_typ _ = I;
-
-fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
-
 
 (** Types **)