quotient_def.ML
changeset 496 8f1bf5266ebc
parent 389 d67240113f68
child 531 3feed4dbfa45
--- 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