--- a/Quot/quotient_def.ML	Thu Jan 14 12:14:35 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Jan 14 12:17:39 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 trm (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end