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)].*)