src/Tools/Code/code_target.ML
changeset 38928 0e6f54c9d201
parent 38927 544f4702d621
child 38929 d9ac9dee764d
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 14:43:27 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 15:08:04 2010 +0200
     1.3 @@ -105,7 +105,6 @@
     1.4      labelled_name: string -> string,
     1.5      reserved_syms: string list,
     1.6      includes: (string * Pretty.T) list,
     1.7 -    single_module: bool,
     1.8      module_alias: string -> string option,
     1.9      class_syntax: string -> string option,
    1.10      tyco_syntax: string -> Code_Printer.tyco_syntax option,
    1.11 @@ -314,7 +313,6 @@
    1.12        labelled_name = Code_Thingol.labelled_name thy proto_program,
    1.13        reserved_syms = reserved,
    1.14        includes = includes,
    1.15 -      single_module = is_some module_name,
    1.16        module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
    1.17        class_syntax = Symtab.lookup class_syntax,
    1.18        tyco_syntax = Symtab.lookup tyco_syntax,