1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Oct 28 22:17:30 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Oct 28 23:10:44 2011 +0200
     1.3 @@ -72,11 +72,13 @@
     1.4      (* data storage *)
     1.5      val qconst_data = {qconst = trm, rconst = rhs, def = thm}
     1.6  
     1.7 -    fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
     1.8 -    fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
     1.9 -    val lthy'' =
    1.10 -      Local_Theory.declaration {syntax = false, pervasive = true}
    1.11 -        (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
    1.12 +    val lthy'' = lthy'
    1.13 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.14 +        (fn phi =>
    1.15 +          (case Quotient_Info.transform_quotconsts phi qconst_data of
    1.16 +            qcinfo as {qconst = Const (c, _), ...} =>
    1.17 +              Quotient_Info.update_quotconsts c qcinfo
    1.18 +          | _ => I));
    1.19    in
    1.20      (qconst_data, lthy'')
    1.21    end