equal
deleted
inserted
replaced
137 |> Syntax.check_term lthy |
137 |> Syntax.check_term lthy |
138 |
138 |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
140 |
140 |
141 val nconst_str = Binding.name_of nconst_bname |
141 val nconst_str = Binding.name_of nconst_bname |
142 val qc_info = {qconst = trm, rconst = rhs} |
142 val qcinfo = {qconst = trm, rconst = rhs} |
143 val lthy'' = qconsts_update nconst_str qc_info lthy' |
143 val lthy'' = LocalTheory.declaration true |
|
144 (fn phi => qconsts_update_generic nconst_str |
|
145 (qconsts_transfer phi qcinfo)) lthy' |
144 in |
146 in |
145 ((trm, thm), lthy'') |
147 ((trm, thm), lthy'') |
146 end |
148 end |
147 |
149 |
148 (* interface and syntax setup *) |
150 (* interface and syntax setup *) |