1.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 13:43:38 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 13:58:16 2010 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    type serialization
     1.5    val parse_args: 'a parser -> Token.T list -> 'a
     1.6    val serialization: (int -> Path.T option -> 'a -> unit)
     1.7 -    -> (bool -> int -> 'a -> string * string option list)
     1.8 +    -> (string list -> int -> 'a -> string * string option list)
     1.9      -> 'a -> serialization
    1.10    val set_default_code_width: int -> theory -> theory
    1.11  
    1.12 @@ -76,8 +76,8 @@
    1.13    | stmt_names_of_destination _ = [];
    1.14  
    1.15  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    1.16 -  | serialization _ string content width Produce = SOME (string false width content)
    1.17 -  | serialization _ string content width (Present _) = SOME (string false width content);
    1.18 +  | serialization _ string content width Produce = SOME (string [] width content)
    1.19 +  | serialization _ string content width (Present _) = SOME (string [] width content);
    1.20  
    1.21  fun export some_path f = (f (Export some_path); ());
    1.22  fun produce f = the (f Produce);