# HG changeset patch
# User wenzelm
# Date 1537782609 -7200
# Node ID 17f9f50e2dbe9f52d31f48a9470df64672c237ab
# Parent  587d0b8a760968dccadd57462548b1661621611d
tuned signature: canonical argument order;

diff -r 587d0b8a7609 -r 17f9f50e2dbe src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 11:45:20 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 11:50:09 2018 +0200
@@ -109,7 +109,7 @@
 type mixin = (morphism * bool) * serial;
 type mixins = mixin list Inttab.table;
 
-fun lookup_mixins serial' (mixins: mixins) = Inttab.lookup_list mixins serial';
+fun lookup_mixins (mixins: mixins) serial' = Inttab.lookup_list mixins serial';
 
 val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =);
 
@@ -228,8 +228,7 @@
 
 fun dependencies_of thy = #dependencies o the_locale thy;
 
-fun mixins_of thy name serial = the_locale thy name |>
-  #mixins |> lookup_mixins serial;
+fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial;
 
 (* FIXME unused!? *)
 fun identity_on thy name morph =
@@ -383,7 +382,7 @@
   in
     (case Idtab.lookup regs (name, instance_of thy name morph) of
       NONE => []
-    | SOME (_, serial) => lookup_mixins serial mixins)
+    | SOME (_, serial) => lookup_mixins mixins serial)
   end;
 
 fun collect_mixins context (name, morph) =