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