605 (name, base $> (collect_mixins context (name, base $> export)) $> export)); |
605 (name, base $> (collect_mixins context (name, base $> export)) $> export)); |
606 |
606 |
607 fun add_dependency loc {inst = (name, morph), mixin, export} thy = |
607 fun add_dependency loc {inst = (name, morph), mixin, export} thy = |
608 let |
608 let |
609 val serial' = serial (); |
609 val serial' = serial (); |
610 val thy' = thy |> |
610 val add_dep = |
611 (change_locale loc o apsnd) |
611 apfst (cons ((name, (morph, export)), serial')) #> |
612 (apfst (cons ((name, (morph, export)), serial')) #> |
612 apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin); |
613 apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin)); |
613 val thy' = change_locale loc (apsnd add_dep) thy; |
614 val context' = Context.Theory thy'; |
614 val context' = Context.Theory thy'; |
615 val (_, regs) = |
615 val (_, regs) = |
616 fold_rev (roundup thy' cons export) |
616 fold_rev (roundup thy' cons export) |
617 (registrations_of context' loc) (Idents.get context', []); |
617 (registrations_of context' loc) (Idents.get context', []); |
618 in |
618 in |
619 thy' |
619 fold_rev (fn inst => add_registration_theory {inst = inst, mixin = NONE, export = export}) |
620 |> fold_rev (fn dep => add_registration_theory {inst = dep, mixin = NONE, export = export}) regs |
620 regs thy' |
621 end; |
621 end; |
622 |
622 |
623 |
623 |
624 (*** Storing results ***) |
624 (*** Storing results ***) |
625 |
625 |