equal
deleted
inserted
replaced
42 val (_, prop') = LocalDefs.cert_def lthy prop |
42 val (_, prop') = LocalDefs.cert_def lthy prop |
43 val (_, newrhs) = Primitive_Defs.abs_def prop' |
43 val (_, newrhs) = Primitive_Defs.abs_def prop' |
44 |
44 |
45 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
45 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
46 |
46 |
47 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
47 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
48 val lthy'' = Local_Theory.declaration true |
48 val lthy'' = Local_Theory.declaration true |
49 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
49 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
50 in |
50 in |
51 ((trm, thm), lthy'') |
51 ((trm, thm), lthy'') |
52 end |
52 end |