# HG changeset patch
# User wenzelm
# Date 1537812341 -7200
# Node ID df6c946cb296ab6771036ddce3b5cff2defd0eb0
# Parent  70f9826753f6255ebdc3007626796daf59b2db70
tuned;

diff -r 70f9826753f6 -r df6c946cb296 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 19:53:45 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 20:05:41 2018 +0200
@@ -607,17 +607,17 @@
 fun add_dependency loc {inst = (name, morph), mixin, export} thy =
   let
     val serial' = serial ();
-    val thy' = thy |>
-      (change_locale loc o apsnd)
-        (apfst (cons ((name, (morph, export)), serial')) #>
-          apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
+    val add_dep =
+      apfst (cons ((name, (morph, export)), serial')) #>
+      apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin);
+    val thy' = change_locale loc (apsnd add_dep) thy;
     val context' = Context.Theory thy';
     val (_, regs) =
       fold_rev (roundup thy' cons export)
         (registrations_of context' loc) (Idents.get context', []);
   in
-    thy'
-    |> fold_rev (fn dep => add_registration_theory {inst = dep, mixin = NONE, export = export}) regs
+    fold_rev (fn inst => add_registration_theory {inst = inst, mixin = NONE, export = export})
+      regs thy'
   end;