diff -r 8a1f4227dff9 -r f178958d3d81 quotient_def.ML
--- a/quotient_def.ML	Fri Dec 04 18:32:19 2009 +0100
+++ b/quotient_def.ML	Fri Dec 04 21:42:55 2009 +0100
@@ -96,10 +96,14 @@
 
   val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
 
-  val qconst_str = Binding.name_of qconst_bname
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy'
+                 (fn phi => 
+                       let
+                         val qconst_str = fst (Term.dest_Const (Morphism.term phi trm))
+                       in                      
+                         qconsts_update_gen qconst_str (qcinfo phi)
+                       end) lthy'
 in
   ((trm, thm), lthy'')
 end