--- a/quotient_def.ML	Thu Dec 03 14:00:43 2009 +0100
+++ b/quotient_def.ML	Thu Dec 03 14:02:05 2009 +0100
@@ -97,7 +97,7 @@
   val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
 
   val qconst_str = Binding.name_of qconst_bname
-  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs}
+  fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
                  (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy'
 in