--- a/quotient_def.ML	Thu Nov 12 02:54:40 2009 +0100
+++ b/quotient_def.ML	Thu Nov 12 12:07:33 2009 +0100
@@ -138,7 +138,7 @@
 
   val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
 
-  val nconst_str = Binding.str_of nconst_bname
+  val nconst_str = Binding.name_of nconst_bname
   val qc_info = {qconst = trm, rconst = rhs}
   val lthy'' = qconsts_update nconst_str qc_info lthy'
 in