--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Oct 28 22:17:30 2011 +0200
@@ -75,7 +75,7 @@
fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
val lthy'' =
- Local_Theory.declaration true
+ Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
in
(qconst_data, lthy'')