--- a/Quot/quotient_def.ML	Wed Dec 30 12:10:57 2009 +0000
+++ b/Quot/quotient_def.ML	Thu Dec 31 23:53:10 2009 +0100
@@ -44,7 +44,7 @@
 
   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
 
-  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
+  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
                  (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
 in