src/Pure/Isar/locale.ML

   lists indexed by registration/dependency serial,
   entries for empty lists may be omitted*)
 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 =);
 
 fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ()));
 

 
 fun hyp_spec_of thy = #hyp_spec o the_locale thy;
 
 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 =
   let val mk_instance = instance_of thy name
   in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end;

     val thy = Context.theory_of context;
     val (regs, mixins) = Registrations.get context;
   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) =
   let
     val thy = Context.theory_of context;