tuned;

--- a/src/Pure/Isar/expression.ML	Sat Mar 10 19:49:32 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 10 20:02:15 2012 +0100
@@ -814,17 +814,15 @@
 
 local
 
-fun note_eqns_register deps witss attrss eqns export export' context =
-  context
-  |> Element.generic_note_thmss Thm.lemmaK
+fun note_eqns_register deps witss attrss eqns export export' =
+  Element.generic_note_thmss Thm.lemmaK
     (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
-  |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
-  |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+  #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
+  #-> (fn eqns => fold (fn ((dep, morph), wits) =>
     fn context =>
-      Locale.add_registration (dep, morph $> Element.satisfy_morphism
-          (map (Element.transform_witness export') wits))
-        (Element.eq_morphism (Context.theory_of context) eqns |>
-          Option.map (rpair true))
+      Locale.add_registration
+        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
+        (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
         export context) (deps ~~ witss));
 
 fun gen_interpretation prep_expr parse_prop prep_attr

--- a/src/Pure/Isar/locale.ML	Sat Mar 10 19:49:32 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 10 20:02:15 2012 +0100
@@ -107,9 +107,9 @@
   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;
@@ -391,7 +391,8 @@
     |> 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) ,_)) =>
@@ -543,8 +544,9 @@
         (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
@@ -674,7 +676,7 @@
 
 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;
@@ -690,7 +692,8 @@
         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;

--- a/src/Tools/interpretation_with_defs.ML	Sat Mar 10 19:49:32 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML	Sat Mar 10 20:02:15 2012 +0100
@@ -17,20 +17,19 @@
 structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
 struct
 
-fun note_eqns_register deps witss def_eqns attrss eqns export export' context =
+fun note_eqns_register deps witss def_eqns attrss eqns export export' =
   let
     fun meta_rewrite context =
       map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
         maps snd;
   in
-    context
-    |> Element.generic_note_thmss Thm.lemmaK
+    Element.generic_note_thmss Thm.lemmaK
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
-    |-> (fn facts => `(fn context => meta_rewrite context facts))
-    |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+    #-> (fn facts => `(fn context => meta_rewrite context facts))
+    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
       fn context =>
-        Locale.add_registration (dep, morph $> Element.satisfy_morphism
-            (map (Element.transform_witness export') wits))
+        Locale.add_registration
+          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
           (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
             Option.map (rpair true))
           export context) (deps ~~ witss))