492 (Symtab.dest (#axioms (Theory.rep_theory thy))); |
492 (Symtab.dest (#axioms (Theory.rep_theory thy))); |
493 |
493 |
494 |
494 |
495 (* name and tags -- make proof objects more readable *) |
495 (* name and tags -- make proof objects more readable *) |
496 |
496 |
497 fun get_name_tags (Thm {prop, der = (_, prf), ...}) = Pt.get_name_tags prop prf; |
497 fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) = |
|
498 Pt.get_name_tags hyps prop prf; |
498 |
499 |
499 fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) = |
500 fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) = |
500 Thm {sign_ref = sign_ref, |
501 Thm {sign_ref = sign_ref, |
501 der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), |
502 der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), |
502 maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop}; |
503 maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop}; |