tuned;
authorwenzelm
Thu Aug 30 14:56:04 2018 +0200 (13 months ago)
changeset 68856e5097a5b2e58
parent 68855 59ce31e15c33
child 68857 b888de4fe58c
tuned;
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 14:48:02 2018 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:56:04 2018 +0200
     1.3 @@ -543,22 +543,19 @@
     1.4    let
     1.5      val thy = Context.theory_of context;
     1.6      val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
     1.7 -    val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
     1.8 -    val morph = base_morph $> mix;
     1.9 -    val inst = instance_of thy name morph;
    1.10 +    val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix);
    1.11 +    val inst = instance_of thy name mix_morph;
    1.12      val idents = Idents.get context;
    1.13    in
    1.14 -    if redundant_ident thy idents (name, inst)
    1.15 -    then context  (* FIXME amend mixins? *)
    1.16 +    if redundant_ident thy idents (name, inst) then context  (* FIXME amend mixins? *)
    1.17      else
    1.18        (idents, context)
    1.19        (* add new registrations with inherited mixins *)
    1.20 -      |> roundup thy (add_reg thy export) export (name, morph)
    1.21 -      |> snd
    1.22 +      |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2
    1.23        (* add mixin *)
    1.24 -      |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
    1.25 +      |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export}
    1.26        (* activate import hierarchy as far as not already active *)
    1.27 -      |> activate_facts (SOME export) (name, morph $> pos_morph)
    1.28 +      |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
    1.29    end;
    1.30  
    1.31  val add_registration_theory = Context.theory_map o add_registration;