1.1 --- a/src/Tools/Code/code_haskell.ML	Mon Aug 30 16:31:38 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Aug 30 16:33:06 2010 +0200
     1.3 @@ -390,7 +390,7 @@
     1.4            end
     1.5        | write_module width NONE (_, content) = writeln_pretty width content;
     1.6    in
     1.7 -    Code_Target.mk_serialization
     1.8 +    Code_Target.serialization
     1.9        (fn width => fn destination => K () o map (write_module width destination))
    1.10        (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
    1.11        (map (uncurry print_module) includes

     2.1 --- a/src/Tools/Code/code_ml.ML	Mon Aug 30 16:31:38 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Mon Aug 30 16:33:06 2010 +0200
     2.3 @@ -937,7 +937,7 @@
     2.4      fun write width NONE = writeln_pretty width
     2.5        | write width (SOME p) = File.write p o string_of_pretty width;
     2.6    in
     2.7 -    Code_Target.mk_serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
     2.8 +    Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
     2.9    end;
    2.10  
    2.11  end; (*local*)

     3.1 --- a/src/Tools/Code/code_scala.ML	Mon Aug 30 16:31:38 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Mon Aug 30 16:33:06 2010 +0200
     3.3 @@ -483,7 +483,7 @@
     3.4      fun write width NONE = writeln_pretty width
     3.5        | write width (SOME p) = File.write p o string_of_pretty width;
     3.6    in
     3.7 -    Code_Target.mk_serialization write (rpair [] oo string_of_pretty) p
     3.8 +    Code_Target.serialization write (rpair [] oo string_of_pretty) p
     3.9    end;
    3.10  
    3.11  end; (*local*)

     4.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:31:38 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:33:06 2010 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    type destination
     4.5    type serialization
     4.6    val parse_args: 'a parser -> Token.T list -> 'a
     4.7 -  val mk_serialization: (int -> Path.T option -> 'a -> unit)
     4.8 +  val serialization: (int -> Path.T option -> 'a -> unit)
     4.9      -> (int -> 'a -> string * string option list)
    4.10      -> 'a -> int -> serialization
    4.11    val serialize: theory -> string -> int option -> string option -> Token.T list
    4.12 @@ -70,8 +70,8 @@
    4.13  fun stmt_names_of_destination (String stmt_names) = stmt_names
    4.14    | stmt_names_of_destination _ = [];
    4.15  
    4.16 -fun mk_serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    4.17 -  | mk_serialization _ string pretty width (String _) = SOME (string width pretty);
    4.18 +fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    4.19 +  | serialization _ string pretty width (String _) = SOME (string width pretty);
    4.20  
    4.21  
    4.22  (** theory data **)