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