892 | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts |
892 | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts |
893 (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd); |
893 (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd); |
894 |
894 |
895 in |
895 in |
896 |
896 |
897 fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt => |
897 fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => |
898 let |
898 let |
899 val name = full_name ctxt b; |
899 val name = full_name ctxt b; |
900 val facts = Global_Theory.name_thmss false name raw_facts; |
900 val facts = Global_Theory.name_thmss false name raw_facts; |
901 fun app (th, attrs) x = |
901 fun app (ths, atts) = |
902 swap (Library.foldl_map |
902 fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; |
903 (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th)); |
|
904 val (res, ctxt') = fold_map app facts ctxt; |
903 val (res, ctxt') = fold_map app facts ctxt; |
905 val thms = Global_Theory.name_thms false false name (flat res); |
904 val thms = Global_Theory.name_thms false false name (flat res); |
906 val Mode {stmt, ...} = get_mode ctxt; |
905 val Mode {stmt, ...} = get_mode ctxt; |
907 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); |
906 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); |
908 |
907 |