equal
deleted
inserted
replaced
521 fun parse_thy (lex, sectab) chs = #1 (!! (theory_defn sectab) (tokenize lex chs)); |
521 fun parse_thy (lex, sectab) chs = #1 (!! (theory_defn sectab) (tokenize lex chs)); |
522 |
522 |
523 |
523 |
524 (* standard sections *) |
524 (* standard sections *) |
525 |
525 |
526 fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";"; |
526 fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", None);"; |
527 val mk_vals = cat_lines o map mk_val; |
527 val mk_vals = cat_lines o map mk_val; |
528 |
528 |
529 fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs) |
529 fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs) |
530 | mk_axm_sect pretxt (txt, axs) = (pretxt ^ "\n" ^ txt, mk_vals axs); |
530 | mk_axm_sect pretxt (txt, axs) = (pretxt ^ "\n" ^ txt, mk_vals axs); |
531 |
531 |