diff -r a6cf197c1f1e -r a2c4adb839a9 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 30 10:50:28 2014 +0200
@@ -39,6 +39,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 typ_subst_nonatomic: (typ * typ) list -> typ -> typ
   val subst_nonatomic_types: (typ * typ) list -> term -> term
 
@@ -177,6 +179,12 @@
   apfst (map TFree) o
     variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
 
+fun name_of_const what t =
+  (case head_of t of
+    Const (s, _) => s
+  | Free (s, _) => s
+  | _ => error ("Cannot extract name of " ^ what));
+
 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
 fun typ_subst_nonatomic [] = I
   | typ_subst_nonatomic inst =