more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Oct 28 22:17:30 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Oct 28 23:10:44 2011 +0200
@@ -72,11 +72,13 @@
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = thm}
- 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 {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
+ val lthy'' = lthy'
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi =>
+ (case Quotient_Info.transform_quotconsts phi qconst_data of
+ qcinfo as {qconst = Const (c, _), ...} =>
+ Quotient_Info.update_quotconsts c qcinfo
+ | _ => I));
in
(qconst_data, lthy'')
end