src/Pure/Isar/locale.ML

 
 fun insert_mixin serial' mixin =
   Inttab.map_default (serial', []) (cons (mixin, serial ()));
 
 fun rename_mixin (old, new) mix =
-  case Inttab.lookup mix old of
-    NONE => mix |
-    SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs);
+  (case Inttab.lookup mix old of
+    NONE => mix
+  | SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs));
 
 fun compose_mixins mixins =
   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
 
 datatype locale = Loc of {

     |> snd |> filter (snd o fst)  (* only inheritable mixins *)
     |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
     |> compose_mixins
   end;
 
-fun get_registrations context select = Registrations.get context
+fun get_registrations context select =
+  Registrations.get context
   |>> Idtab.dest |>> select
   (* with inherited mixins *)
   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
     (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
 

     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 context' = Context.Theory thy';
-    val (_, regs) = fold_rev (roundup thy' cons export)
-      (registrations_of context' loc) (get_idents (context'), []);
+    val (_, regs) =
+      fold_rev (roundup thy' cons export)
+        (registrations_of context' loc) (get_idents (context'), []);
   in
     thy'
     |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   end;
 

     | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
   end |> Pretty.writeln;
 
 fun locale_deps thy =
   let
-    val names = all_locales thy
+    val names = all_locales thy;
     fun add_locale_node name =
       let
         val params = params_of thy name;
         val axioms =
           these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));

     fun add_locale_deps name =
       let
         val dependencies =
           map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
       in
-        fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
+        fold (fn (super, ts) => fn (gr, deps) =>
+         (gr |> Graph.add_edge (super, name),
           deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
             dependencies
       end;
   in
     Graph.empty