258 map (Sign.pretty_term sg) ts @ |
258 map (Sign.pretty_term sg) ts @ |
259 map (Sign.pretty_typ sg o TVar) ixns))))); |
259 map (Sign.pretty_typ sg o TVar) ixns))))); |
260 |
260 |
261 fun cert_axm sg (name, raw_tm) = |
261 fun cert_axm sg (name, raw_tm) = |
262 let |
262 let |
263 val (t, T, _) = Sign.certify_term sg raw_tm |
263 val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm |
264 handle TYPE (msg, _, _) => error msg |
264 handle TYPE (msg, _, _) => error msg |
265 | TERM (msg, _) => error msg; |
265 | TERM (msg, _) => error msg; |
266 in |
266 in |
267 Term.no_dummy_patterns t handle TERM (msg, _) => error msg; |
267 Term.no_dummy_patterns t handle TERM (msg, _) => error msg; |
268 assert (T = propT) "Term not of type prop"; |
268 assert (T = propT) "Term not of type prop"; |
271 |
271 |
272 (*some duplication of code with read_def_cterm*) |
272 (*some duplication of code with read_def_cterm*) |
273 fun read_def_axm (sg, types, sorts) used (name, str) = |
273 fun read_def_axm (sg, types, sorts) used (name, str) = |
274 let |
274 let |
275 val ts = Syntax.read (Sign.syn_of sg) propT str; |
275 val ts = Syntax.read (Sign.syn_of sg) propT str; |
276 val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); |
276 val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT); |
277 in cert_axm sg (name, t) end |
277 in cert_axm sg (name, t) end |
278 handle ERROR => err_in_axm name; |
278 handle ERROR => err_in_axm name; |
279 |
279 |
280 fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; |
280 fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; |
281 |
281 |
282 fun inferT_axm sg (name, pre_tm) = |
282 fun inferT_axm sg (name, pre_tm) = |
283 let |
283 let val (t, _) = Sign.infer_types (Sign.pp sg) sg |
284 val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT); |
284 (K None) (K None) [] true ([pre_tm], propT); |
285 in (name, no_vars sg t) end |
285 in (name, no_vars sg t) end |
286 handle ERROR => err_in_axm name; |
286 handle ERROR => err_in_axm name; |
287 |
287 |
288 |
288 |
289 (* extend axioms of a theory *) |
289 (* extend axioms of a theory *) |
508 make_theory sign const_deps final_consts' axioms oracles parents ancestors |
508 make_theory sign const_deps final_consts' axioms oracles parents ancestors |
509 end; |
509 end; |
510 |
510 |
511 local |
511 local |
512 fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; |
512 fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; |
513 val cert_term = #1 oo Sign.certify_term; |
513 fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg; |
514 in |
514 in |
515 val add_finals = ext_finals read_term; |
515 val add_finals = ext_finals read_term; |
516 val add_finals_i = ext_finals cert_term; |
516 val add_finals_i = ext_finals cert_term; |
517 end; |
517 end; |
518 |
518 |