equal
deleted
inserted
replaced
95 |> Syntax.check_term lthy |
95 |> Syntax.check_term lthy |
96 |
96 |
97 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
97 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
98 |
98 |
99 val qconst_str = Binding.name_of qconst_bname |
99 val qconst_str = Binding.name_of qconst_bname |
100 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs} |
100 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
101 val lthy'' = Local_Theory.declaration true |
101 val lthy'' = Local_Theory.declaration true |
102 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy' |
102 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy' |
103 in |
103 in |
104 ((trm, thm), lthy'') |
104 ((trm, thm), lthy'') |
105 end |
105 end |