1.1 --- a/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:29:38 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:55:54 2010 +0200
     1.3 @@ -313,8 +313,8 @@
     1.4        handle Option => error ("Unknown statement name: " ^ labelled_name name);
     1.5    in (deresolver, hs_program) end;
     1.6  
     1.7 -fun serialize_haskell module_prefix module_name string_classes labelled_name
     1.8 -    raw_reserved includes module_alias
     1.9 +fun serialize_haskell module_prefix string_classes labelled_name
    1.10 +    raw_reserved includes single_module module_alias
    1.11      class_syntax tyco_syntax const_syntax program
    1.12      (stmt_names, presentation_stmt_names) =
    1.13    let
    1.14 @@ -350,7 +350,7 @@
    1.15      fun serialize_module1 (module_name', (deps, (stmts, _))) =
    1.16        let
    1.17          val stmt_names = map fst stmts;
    1.18 -        val qualified = is_none module_name;
    1.19 +        val qualified = not single_module;
    1.20          val imports = subtract (op =) stmt_names deps
    1.21            |> distinct (op =)
    1.22            |> map_filter (try deresolver)
    1.23 @@ -465,11 +465,11 @@
    1.24  
    1.25  (** Isar setup **)
    1.26  
    1.27 -fun isar_serializer module_name =
    1.28 +val isar_serializer =
    1.29    Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
    1.30      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
    1.31      >> (fn (module_prefix, string_classes) =>
    1.32 -      serialize_haskell module_prefix module_name string_classes));
    1.33 +      serialize_haskell module_prefix string_classes));
    1.34  
    1.35  val _ =
    1.36    Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (