Quot/quotient_def.ML
changeset 868 09d5b7f0e55d
parent 864 999870716cc8
child 869 ce5f78f0eac5
equal deleted inserted replaced
867:9e247b9505f0 868:09d5b7f0e55d
    50   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
    50   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
    51 
    51 
    52   (* data storage *)
    52   (* data storage *)
    53   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
    53   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
    54   val lthy'' = Local_Theory.declaration true
    54   val lthy'' = Local_Theory.declaration true
    55                  (fn phi => qconsts_update_gen trm (qcinfo phi)) lthy'
    55                  (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
    56 in
    56 in
    57   ((trm, thm), lthy'')
    57   ((trm, thm), lthy'')
    58 end
    58 end
    59 
    59 
    60 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
    60 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =