diff -r d3c7f6d19c7f -r 746b17e1d6d8 quotient_def.ML
--- a/quotient_def.ML	Fri Nov 13 19:32:12 2009 +0100
+++ b/quotient_def.ML	Wed Nov 18 23:52:48 2009 +0100
@@ -139,8 +139,10 @@
   val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
 
   val nconst_str = Binding.name_of nconst_bname
-  val qc_info = {qconst = trm, rconst = rhs}
-  val lthy'' = qconsts_update nconst_str qc_info lthy'
+  val qcinfo = {qconst = trm, rconst = rhs}
+  val lthy'' = LocalTheory.declaration true
+                (fn phi => qconsts_update_generic nconst_str 
+                             (qconsts_transfer phi qcinfo)) lthy'
 in
   ((trm, thm), lthy'')
 end