diff -r 76fa93b1fe8b -r 8f1bf5266ebc quotient_def.ML
--- a/quotient_def.ML	Thu Dec 03 11:58:46 2009 +0100
+++ b/quotient_def.ML	Thu Dec 03 12:17:23 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