equal
deleted
inserted
replaced
717 |
717 |
718 |
718 |
719 (* global_qed *) |
719 (* global_qed *) |
720 |
720 |
721 fun locale_prefix None f thy = f thy |
721 fun locale_prefix None f thy = f thy |
722 | locale_prefix (Some (loc, _)) f thy = thy |> Theory.add_path loc |> f |>> Theory.parent_path; |
722 | locale_prefix (Some (loc, _)) f thy = |
|
723 thy |> Theory.add_path (Sign.base_name loc) |> f |>> Theory.parent_path; |
723 |
724 |
724 fun locale_store_thm _ None _ = I |
725 fun locale_store_thm _ None _ = I |
725 | locale_store_thm name (Some (loc, atts)) th = Locale.store_thm loc ((name, th), atts); |
726 | locale_store_thm name (Some (loc, atts)) th = Locale.store_thm loc ((name, th), atts); |
726 |
727 |
727 fun finish_global state = |
728 fun finish_global state = |