src/Pure/codegen.ML

     Pretty.writeln (Pretty.chunks
       [Pretty.strs ("term code generators:" :: map fst codegens),
        Pretty.strs ("type code generators:" :: map fst tycodegens)]);
 end);
 
-val _ = Context.add_setup [CodegenData.init];
+val _ = Context.add_setup CodegenData.init;
 val print_codegens = CodegenData.print;
 
 
 (**** access parameters for random testing ****)
 

 val code_attr =
   Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
     (#attrs (CodegenData.get thy)))));
 
 val _ = Context.add_setup
- [Attrib.add_attributes
+ (Attrib.add_attributes
   [("code", (code_attr, K Attrib.undef_local_attribute),
-     "declare theorems for code generation")]];
+     "declare theorems for code generation")]);
 
 
 (**** preprocessors ****)
 
 fun add_preprocessor p thy =

         then rewrite_rule [eqn] (Thm.transfer thy th)
         else th
       end)
   in (add_preprocessor prep thy, eqn) end;
 
-val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];
+val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
 
 
 (**** associate constants with target language code ****)
 
 fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>

              | SOME (_, module'', _) =>
                  (add_edge (node_id, dep) gr'', p module''))
            end);
 
 val _ = Context.add_setup
- [add_codegen "default" default_codegen,
-  add_tycodegen "default" default_tycodegen];
+ (add_codegen "default" default_codegen #>
+  add_tycodegen "default" default_tycodegen);
 
 
 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
 
 fun add_to_module name s = AList.map_entry (op =) name (suffix s);

        (Symbol.explode s) of
      (p, []) => p
    | _ => error ("Malformed annotation: " ^ quote s));
 
 val _ = Context.add_setup
-  [assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
+  (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
      [("term_of",
        "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
       ("test",
        "fun gen_fun_type _ G i =\n\
        \  let\n\

        \    val _ = (f := (fn x =>\n\
        \      let\n\
        \        val y = G i;\n\
        \        val f' = !f\n\
        \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
-       \  in (fn x => !f x) end;\n")]))]];
+       \  in (fn x => !f x) end;\n")]))]);
 
 
 structure P = OuterParse and K = OuterKeyword;
 
 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")