# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID f9b6af3017fd48e81cb926ea31c48dfdda7317f3
# Parent  71d74e641538a57d2e091b6f3c76ac99cec78518
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')

diff -r 71d74e641538 -r f9b6af3017fd src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -306,7 +306,7 @@
     HOLogic.mk_Trueprop (prem $ t $ u)
   end;
 
-val name_of_set = name_of_const "set";
+val name_of_set = name_of_const "set function" domain_type;
 
 val mp_conj = @{thm mp_conj};
 
@@ -779,7 +779,7 @@
       let
         fun mk_disc_concl disc = [name_of_disc disc];
         fun mk_ctr_concl 0 _ = []
-          | mk_ctr_concl _ ctor = [name_of_ctr ctor];
+          | mk_ctr_concl _ ctr = [name_of_ctr ctr];
         val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
         val ctr_concls = map2 mk_ctr_concl ms ctrs;
       in
@@ -1771,7 +1771,7 @@
                     |> singleton (Proof_Context.export names_lthy lthy)
                     |> Thm.close_derivation;
 
-                  val ctr_names = quasi_unambiguous_case_names ((map name_of_ctr) ctrAs);
+                  val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs);
                   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
                   val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
                   val cases_pred_attr = Attrib.internal o K o Induct.cases_pred;
diff -r 71d74e641538 -r f9b6af3017fd src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -127,8 +127,6 @@
 
   val co_prefix: BNF_Util.fp_kind -> string
 
-  val base_name_of_typ: typ -> string
-
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
@@ -348,12 +346,6 @@
 
 fun co_prefix fp = case_fp fp "" "co";
 
-fun add_components_of_typ (Type (s, Ts)) =
-    cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
-  | add_components_of_typ _ = I;
-
-fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
-
 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
 
 val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
diff -r 71d74e641538 -r f9b6af3017fd src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -281,7 +281,7 @@
 fun mk_disc_or_sel Ts t =
   subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
 
-val name_of_ctr = name_of_const "constructor";
+val name_of_ctr = name_of_const "constructor" body_type;
 
 fun name_of_disc t =
   (case head_of t of
@@ -291,7 +291,7 @@
     Long_Name.map_base_name (prefix isN) (name_of_disc t')
   | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
     Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
-  | t' => name_of_const "destructor" t');
+  | t' => name_of_const "discriminator" domain_type t');
 
 val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
 
diff -r 71d74e641538 -r f9b6af3017fd src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -40,7 +40,8 @@
     (string * sort) list * Proof.context
   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
 
-  val name_of_const: string -> term -> string
+  val base_name_of_typ: typ -> string
+  val name_of_const: string -> (typ -> typ) -> term -> string
 
   val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
   val subst_nonatomic_types: (typ * typ) list -> term -> term
@@ -198,10 +199,20 @@
   apfst (map TFree) o
     variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
 
-fun name_of_const what t =
+fun add_components_of_typ (Type (s, Ts)) =
+    cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
+  | add_components_of_typ _ = I;
+
+fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
+
+fun suffix_with_type s (Type (_, Ts)) =
+    space_implode "_" (s :: fold_rev add_components_of_typ Ts [])
+  | suffix_with_type s _ = s;
+
+fun name_of_const what get_fcT t =
   (case head_of t of
-    Const (s, _) => s
-  | Free (s, _) => s
+    Const (s, T) => suffix_with_type s (get_fcT T)
+  | Free (s, T) => suffix_with_type s (get_fcT T)
   | _ => error ("Cannot extract name of " ^ what));
 
 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)