# HG changeset patch
# User wenzelm
# Date 1331499972 -3600
# Node ID 11050f8e5f8e7f8925a29f3f468a68fa2d03534a
# Parent  26a9a4e0a631ac6807b04bd95ab2f3ae5b389724
tuned;

diff -r 26a9a4e0a631 -r 11050f8e5f8e src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Mar 11 14:09:01 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Mar 11 22:06:12 2012 +0100
@@ -291,7 +291,7 @@
 in
 
 (* Note that while identifiers always have the external (exported) view, activate_dep
-  is presented with the internal view. *)
+   is presented with the internal view. *)
 
 fun roundup thy activate_dep export (name, morph) (marked, input) =
   let
@@ -488,13 +488,9 @@
     else
       (Idents.get context, context)
       (* add new registrations with inherited mixins *)
-      |> roundup thy (add_reg thy export) export (name, morph)
-      |> snd
+      |> (snd o roundup thy (add_reg thy export) export (name, morph))
       (* add mixin *)
-      |>
-        (case mixin of
-          NONE => I
-        | SOME mixin => amend_registration (name, morph) mixin export)
+      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)
       |> activate_facts (SOME export) (name, morph)
   end;