src/Tools/Code/code_target.ML
changeset 38916 c0b857a04758
parent 38914 0a49a34e5d37
child 38917 c7da3cc88135
--- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:31:38 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:33:06 2010 +0200
@@ -22,7 +22,7 @@
   type destination
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
-  val mk_serialization: (int -> Path.T option -> 'a -> unit)
+  val serialization: (int -> Path.T option -> 'a -> unit)
     -> (int -> 'a -> string * string option list)
     -> 'a -> int -> serialization
   val serialize: theory -> string -> int option -> string option -> Token.T list
@@ -70,8 +70,8 @@
 fun stmt_names_of_destination (String stmt_names) = stmt_names
   | stmt_names_of_destination _ = [];
 
-fun mk_serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
-  | mk_serialization _ string pretty width (String _) = SOME (string width pretty);
+fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
+  | serialization _ string pretty width (String _) = SOME (string width pretty);
 
 
 (** theory data **)