# HG changeset patch
# User wenzelm
# Date 1319836244 -7200
# Node ID 90106a351a11535e08b177c0e52851d5f53bc759
# Parent  57cd50f98fdcbee3decfcb3559b648a2a25814d5
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);

diff -r 57cd50f98fdc -r 90106a351a11 src/HOL/Tools/Quotient/quotient_def.ML
--- 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