equal
deleted
inserted
replaced
836 |
836 |
837 (* facts *) |
837 (* facts *) |
838 |
838 |
839 fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname)) |
839 fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname)) |
840 | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts |
840 | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts |
841 (Facts.add do_props (naming_of ctxt) (full_name ctxt bname, ths)); |
841 (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths)); |
842 |
842 |
843 fun put_thms do_props thms ctxt = |
843 fun put_thms do_props thms ctxt = |
844 ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt; |
844 ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt; |
845 |
845 |
846 local |
846 local |