diff -r 77fc6f3c0343 -r 4cf79f70efec quotient_def.ML --- 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