equal
deleted
inserted
replaced
48 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
48 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
49 |
49 |
50 (* data storage *) |
50 (* data storage *) |
51 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
51 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
52 val lthy'' = Local_Theory.declaration true |
52 val lthy'' = Local_Theory.declaration true |
53 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
53 (fn phi => qconsts_update_gen trm (qcinfo phi)) lthy' |
54 in |
54 in |
55 ((trm, thm), lthy'') |
55 ((trm, thm), lthy'') |
56 end |
56 end |
57 |
57 |
58 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
58 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |