tuned;

--- a/src/Pure/Isar/expression.ML	Sat Nov 19 14:31:43 2011 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Nov 19 15:04:36 2011 +0100
@@ -354,8 +354,9 @@
       let
         val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
         val inst' = prep_inst ctxt parm_names inst;
-        val parm_types' = map (Type_Infer.paramify_vars o
-          Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
+        val parm_types' = parm_types
+          |> map (Type_Infer.paramify_vars o
+              Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
         val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
@@ -836,7 +837,7 @@
       |> prep_expr expression;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
-    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
+    val attrss = map (apsnd (map (prep_attr theory)) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
@@ -856,7 +857,7 @@
     val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
-    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
+    val attrss = map (apsnd (map (prep_attr theory)) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
@@ -915,7 +916,7 @@
     val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
-    val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
+    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 

--- a/src/Pure/Isar/locale.ML	Sat Nov 19 14:31:43 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Nov 19 15:04:36 2011 +0100
@@ -462,7 +462,8 @@
 fun activate_facts export dep context =
   let
     val thy = Context.theory_of context;
-    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
+    val activate =
+      activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
   in
     roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
       dep (get_idents context, context)
@@ -688,7 +689,7 @@
     fun add_locale_deps name =
       let
         val dependencies =
-          (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name |> map fst);
+          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),
           deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))