equal
deleted
inserted
replaced
49 |
49 |
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 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
54 val lthy'' = Local_Theory.declaration true |
55 val lthy'' = Local_Theory.declaration true |
55 (fn phi => qconsts_update_gen trm (qcinfo phi)) lthy' |
56 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
56 in |
57 in |
57 ((trm, thm), lthy'') |
58 ((trm, thm), lthy'') |
58 end |
59 end |
59 |
60 |
60 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
61 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |