--- a/Nominal/Nominal2.thy	Thu Dec 16 08:42:48 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Dec 17 00:39:27 2010 +0000
@@ -206,7 +206,7 @@
       |> map prop_of
       |> map Logic.strip_horn
       |> split_list
-      |>> map (map strip_params_prems_concl)     
+      |>> (map o map) strip_params_prems_concl     
 
     val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss)
   in
@@ -314,7 +314,7 @@
 
   fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys)
 in
-  map (map (map rawify_bclause)) bclauses
+  (map o map o map) rawify_bclause bclauses
 end
 *}
 
@@ -390,7 +390,7 @@
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
  
   val raw_cns_info = all_dtyp_constrs_types descr sorts
-  val raw_constrs = map (map (fn (c, _, _, _) => c)) raw_cns_info
+  val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info
 
   val raw_inject_thms = flat (map #inject dtinfos)
   val raw_distinct_thms = flat (map #distinct dtinfos)
@@ -630,7 +630,7 @@
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
-  val qtrms = map (map #qconst) qconstrs_infos
+  val qtrms = (map o map) #qconst qconstrs_infos
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
@@ -860,7 +860,7 @@
 let
   val annos_bclauses =
     get_cnstrs dt_strs
-    |> map (map (fn (_, antys, _, bns) => (map fst antys, bns)))
+    |> (map o map) (fn (_, antys, _, bns) => (map fst antys, bns))
 
   fun prep_binder env bn_str =
     case (Syntax.read_term_global thy bn_str) of
@@ -885,7 +885,7 @@
     map (prep_bclause env) bclause_strs
   end
 in
-  (map (map prep_bclauses) annos_bclauses, thy)
+  ((map o map) prep_bclauses annos_bclauses, thy)
 end
 *}
 
@@ -909,7 +909,7 @@
 let
   val args = 
     get_cnstrs dt_strs
-    |> map (map (fn (_, antys, _, _) => length antys))
+    |> (map o map) (fn (_, antys, _, _) => length antys)
 
   fun complt n bcs = 
   let