src/HOL/Tools/Quotient/quotient_def.ML
changeset 45291 57cd50f98fdc
parent 45279 89a17197cb98
child 45292 90106a351a11
equal deleted inserted replaced
45290:f599ac41e7f5 45291:57cd50f98fdc
    73     val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    73     val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    74 
    74 
    75     fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
    75     fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
    76     fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
    76     fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
    77     val lthy'' =
    77     val lthy'' =
    78       Local_Theory.declaration true
    78       Local_Theory.declaration {syntax = false, pervasive = true}
    79         (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
    79         (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
    80   in
    80   in
    81     (qconst_data, lthy'')
    81     (qconst_data, lthy'')
    82   end
    82   end
    83 
    83