equal
deleted
inserted
replaced
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 = |