# HG changeset patch
# User wenzelm
# Date 1535633764 -7200
# Node ID e5097a5b2e58d5dc3edc8dd373ba8889388557e3
# Parent  59ce31e15c33c7c54516b72c8b219072bdb31f35
tuned;

diff -r 59ce31e15c33 -r e5097a5b2e58 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 30 14:48:02 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:56:04 2018 +0200
@@ -543,22 +543,19 @@
   let
     val thy = Context.theory_of context;
     val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
-    val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
-    val morph = base_morph $> mix;
-    val inst = instance_of thy name morph;
+    val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix);
+    val inst = instance_of thy name mix_morph;
     val idents = Idents.get context;
   in
-    if redundant_ident thy idents (name, inst)
-    then context  (* FIXME amend mixins? *)
+    if redundant_ident thy idents (name, inst) then context  (* FIXME amend mixins? *)
     else
       (idents, context)
       (* add new registrations with inherited mixins *)
-      |> roundup thy (add_reg thy export) export (name, morph)
-      |> snd
+      |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2
       (* add mixin *)
-      |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
+      |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export}
       (* activate import hierarchy as far as not already active *)
-      |> activate_facts (SOME export) (name, morph $> pos_morph)
+      |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
   end;
 
 val add_registration_theory = Context.theory_map o add_registration;