equal
deleted
inserted
replaced
540 generated, and it will not be possible to amend it. *) |
540 generated, and it will not be possible to amend it. *) |
541 |
541 |
542 fun add_registration {dep = (name, base_morph), mixin, export} context = |
542 fun add_registration {dep = (name, base_morph), mixin, export} context = |
543 let |
543 let |
544 val thy = Context.theory_of context; |
544 val thy = Context.theory_of context; |
|
545 val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ())); |
545 val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix); |
546 val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix); |
546 val morph = base_morph $> mix; |
547 val morph = base_morph $> mix; |
547 val inst = instance_of thy name morph; |
548 val inst = instance_of thy name morph; |
548 val idents = Idents.get context; |
549 val idents = Idents.get context; |
549 in |
550 in |
555 |> roundup thy (add_reg thy export) export (name, morph) |
556 |> roundup thy (add_reg thy export) export (name, morph) |
556 |> snd |
557 |> snd |
557 (* add mixin *) |
558 (* add mixin *) |
558 |> amend_registration {dep = (name, morph), mixin = mixin, export = export} |
559 |> amend_registration {dep = (name, morph), mixin = mixin, export = export} |
559 (* activate import hierarchy as far as not already active *) |
560 (* activate import hierarchy as far as not already active *) |
560 |> activate_facts (SOME export) (name, morph) |
561 |> activate_facts (SOME export) (name, morph $> pos_morph) |
561 end; |
562 end; |
562 |
563 |
563 val add_registration_theory = Context.theory_map o add_registration; |
564 val add_registration_theory = Context.theory_map o add_registration; |
564 |
565 |
565 fun add_registration_proof registration ctxt = ctxt |
566 fun add_registration_proof registration ctxt = ctxt |