diff -r 09d5b7f0e55d -r ce5f78f0eac5 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Thu Jan 14 08:02:20 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Jan 14 10:06:29 2010 +0100
@@ -51,8 +51,9 @@
 
   (* data storage *)
   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
+  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end