diff --git a/src/Pure/Tools/generated_files.ML b/src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML
+++ b/src/Pure/Tools/generated_files.ML
@@ -1,377 +1,391 @@
 (*  Title:      Pure/Tools/generated_files.ML
     Author:     Makarius
 
 Generated source files for other languages: with antiquotations, without Isabelle symbols.
 *)
 
 signature GENERATED_FILES =
 sig
   val add_files: Path.binding * string -> theory -> theory
   type file = {path: Path.T, pos: Position.T, content: string}
   val file_binding: file -> Path.binding
   val file_markup: file -> Markup.T
   val print_file: file -> string
   val report_file: Proof.context -> Position.T -> file -> unit
   val get_files: theory -> file list
   val get_file: theory -> Path.binding -> file
   val get_files_in: Path.binding list * theory -> (file * Position.T) list
   val check_files_in: Proof.context ->
     (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
   val write_file: Path.T -> file -> unit
   val export_file: theory -> file -> unit
   type file_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
     binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
     theory -> theory
   val antiquotation: binding -> 'a Token.context_parser ->
     ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
     theory -> theory
   val set_string: string -> Proof.context -> Proof.context
   val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
   val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
   val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
   val export_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list -> unit
   val with_compile_dir: (Path.T -> unit) -> unit
   val compile_generated_files: Proof.context ->
     (Path.binding list * theory) list ->
     (Path.T list * Path.T) list ->
     (Path.binding list * bool option) list ->
     Path.binding -> Input.source -> unit
   val compile_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list ->
     ((string * Position.T) list * (string * Position.T)) list ->
     ((string * Position.T) list * bool option) list ->
     string * Position.T -> Input.source -> unit
   val execute: Path.T -> Input.source -> string -> string
 end;
 
 structure Generated_Files: GENERATED_FILES =
 struct
 
 (** context data **)
 
 type file_type =
   {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
 
 type antiquotation = Token.src -> Proof.context -> file_type -> string;
 
+fun err_dup_files path pos pos' =
+  error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']);
+
 structure Data = Theory_Data
 (
   type T =
     (Path.T * (Position.T * string)) list *  (*files for current theory*)
     file_type Name_Space.table *  (*file types*)
     antiquotation Name_Space.table;  (*antiquotations*)
   val empty =
     ([],
      Name_Space.empty_table Markup.file_typeN,
      Name_Space.empty_table Markup.antiquotationN);
-  val extend = @{apply 3(1)} (K []);
-  fun merge ((_, types1, antiqs1), (_, types2, antiqs2)) =
-    ([],
-     Name_Space.merge_tables (types1, types2),
-     Name_Space.merge_tables (antiqs1, antiqs2));
+  val extend = I;
+  fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
+    let
+      val files' = (files1, files2)
+        |> Library.merge (fn ((path1, file1), (path2, file2)) =>
+          if path1 <> path2 then false
+          else if file1 = file2 then true
+          else err_dup_files path1 (#1 file1) (#1 file2));
+      val types' = Name_Space.merge_tables (types1, types2);
+      val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2);
+    in (files', types', antiqs') end;
 );
 
 fun add_files (binding, content) =
   let
     val _ = Path.proper_binding binding;
     val (path, pos) = Path.dest_binding binding;
   in
     (Data.map o @{apply 3(1)}) (fn files =>
       (case AList.lookup (op =) files path of
-        SOME (pos', _) =>
-          error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos'])
+        SOME (pos', _) => err_dup_files path pos pos'
       | NONE => (path, (pos, content)) :: files))
   end;
 
+fun reset_files thy =
+  if null (#1 (Data.get thy)) then NONE
+  else SOME (Data.map (@{apply 3(1)} (K [])) thy);
+
+val _ = Theory.setup (Theory.at_begin reset_files);
+
 
 (* get files *)
 
 type file = {path: Path.T, pos: Position.T, content: string};
 
 fun file_binding (file: file) = Path.binding (#path file, #pos file);
 
 fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file));
 
 fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file)));
 
 fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file);
 
 
 fun get_files thy =
   Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) =>
     {path = path, pos = pos, content = content}: file);
 
 fun get_file thy binding =
   let val (path, pos) = Path.dest_binding binding in
     (case find_first (fn file => #path file = path) (get_files thy) of
       SOME file => file
     | NONE =>
         error ("Missing generated file " ^ Path.print path ^
           " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
   end;
 
 fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy)
   | get_files_in (files, thy) =
       map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files;
 
 
 (* check and output files *)
 
 fun check_files_in ctxt (files, opt_thy) =
   let
     val thy =
       (case opt_thy of
         SOME name => Theory.check {long = false} ctxt name
       | NONE => Proof_Context.theory_of ctxt);
   in (map Path.explode_binding files, thy) end;
 
 fun write_file dir (file: file) =
   let
     val path = Path.expand (Path.append dir (#path file));
     val _ = Isabelle_System.mkdirs (Path.dir path);
     val _ = File.generate path (#content file);
   in () end;
 
 fun export_file thy (file: file) =
   Export.export thy (file_binding file) [XML.Text (#content file)];
 
 
 (* file types *)
 
 fun get_file_type thy ext =
   if ext = "" then error "Bad file extension"
   else
     (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
       (fn (_, file_type) => fn res =>
         if #ext file_type = ext then SOME file_type else res)
     |> (fn SOME file_type => file_type
          | NONE => error ("Unknown file type for extension " ^ quote ext));
 
 fun file_type binding {ext, make_comment, make_string} thy =
   let
     val name = Binding.name_of binding;
     val pos = Binding.pos_of binding;
     val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
 
     val table = #2 (Data.get thy);
     val space = Name_Space.space_of_table table;
     val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
     val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
 
     val _ =
       (case try (#name o get_file_type thy) ext of
         NONE => ()
       | SOME name' =>
           error ("Extension " ^ quote ext ^ " already registered for file type " ^
             quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
   in thy |> (Data.map o @{apply 3(2)}) (K data') end;
 
 
 (* antiquotations *)
 
 val get_antiquotations = #3 o Data.get o Proof_Context.theory_of;
 
 fun antiquotation name scan body thy =
   let
     fun ant src ctxt file_type : string =
       let val (x, ctxt') = Token.syntax scan src ctxt
       in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
   in
     thy
     |> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
   end;
 
 val scan_antiq =
   Antiquote.scan_control >> Antiquote.Control ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
 
 fun read_source ctxt (file_type: file_type) source =
   let
     val _ =
       Context_Position.report ctxt (Input.pos_of source)
         (Markup.language
           {name = #name file_type, symbols = false, antiquotes = true,
             delimited = Input.is_delimited source});
 
     val (input, _) =
       Input.source_explode source
       |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
 
     val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
 
     fun expand antiq =
       (case antiq of
         Antiquote.Text s => s
       | Antiquote.Control {name, body, ...} =>
           let
             val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
             val (src', ant) = Token.check_src ctxt get_antiquotations src;
           in ant src' ctxt file_type end
       | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
   in implode (map expand input) end;
 
 
 
 (** Isar commands **)
 
 (* generate_file *)
 
 fun generate_file (binding, source) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
     val (path, pos) = Path.dest_binding binding;
     val file_type =
       get_file_type thy (#2 (Path.split_ext path))
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
     val content = header ^ "\n" ^ read_source lthy file_type source;
   in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
 
 fun generate_file_cmd (file, source) lthy =
   generate_file (Path.explode_binding file, source) lthy;
 
 
 (* export_generated_files *)
 
 fun export_generated_files ctxt args =
   let val thy = Proof_Context.theory_of ctxt in
     (case map #1 (maps get_files_in args) of
       [] => ()
     | files =>
        (List.app (export_file thy) files;
         writeln (Export.message thy Path.current);
         writeln (cat_lines (map (prefix "  " o print_file) files))))
   end;
 
 fun export_generated_files_cmd ctxt args =
   export_generated_files ctxt (map (check_files_in ctxt) args);
 
 
 (* compile_generated_files *)
 
 val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
 
 fun with_compile_dir body : unit =
   body (Path.explode (Config.get (Context.the_local_context ()) compile_dir));
 
 fun compile_generated_files ctxt args external export export_prefix source =
   Isabelle_System.with_tmp_dir "compile" (fn dir =>
     let
       val thy = Proof_Context.theory_of ctxt;
 
       val files = maps get_files_in args;
       val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
       val _ = List.app (write_file dir o #1) files;
       val _ =
         external |> List.app (fn (files, base_dir) =>
           files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
       val _ =
         ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
           ML_Compiler.flags (Input.pos_of source)
           (ML_Lex.read "Generated_Files.with_compile_dir (" @
             ML_Lex.read_source source @ ML_Lex.read ")");
       val _ =
         export |> List.app (fn (bindings, executable) =>
           bindings |> List.app (fn binding0 =>
             let
               val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
                 (case try File.read (Path.append dir path) of
                   SOME context => context
                 | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
               val _ = Export.report_export thy export_prefix;
               val binding' =
                 Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
             in
               (if is_some executable then Export.export_executable else Export.export)
                 thy binding' [XML.Text content]
             end));
       val _ =
         if null export then ()
         else writeln (Export.message thy (Path.path_of_binding export_prefix));
     in () end);
 
 fun compile_generated_files_cmd ctxt args external export export_prefix source =
   compile_generated_files ctxt
     (map (check_files_in ctxt) args)
     (external |> map (fn (raw_files, raw_base_dir) =>
       let
         val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
         fun check (s, pos) = (Resources.check_file ctxt (SOME base_dir) (s, pos); Path.explode s);
         val files = map check raw_files;
       in (files, base_dir) end))
     ((map o apfst o map) Path.explode_binding export)
     (Path.explode_binding export_prefix)
     source;
 
 
 (* execute compiler -- auxiliary *)
 
 fun execute dir title compile =
   Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile)
     handle ERROR msg =>
       let val (s, pos) = Input.source_content title
       in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;
 
 
 
 (** concrete file types **)
 
 val _ =
   Theory.setup
     (file_type \<^binding>\<open>Haskell\<close>
       {ext = "hs",
        make_comment = enclose "{-" "-}",
        make_string = GHC.print_string});
 
 
 
 (** concrete antiquotations **)
 
 (* ML expression as string literal *)
 
 structure Local_Data = Proof_Data
 (
   type T = string option;
   fun init _ = NONE;
 );
 
 val set_string = Local_Data.put o SOME;
 
 fun the_string ctxt =
   (case Local_Data.get ctxt of
     SOME s => s
   | NONE => raise Fail "No result string");
 
 val _ =
   Theory.setup
     (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
       (fn {context = ctxt, file_type, argument, ...} =>
         ctxt |> Context.proof_map
           (ML_Context.expression (Input.pos_of argument)
             (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @
              ML_Lex.read_source argument @ ML_Lex.read "))"))
         |> the_string |> #make_string file_type));
 
 
 (* file-system paths *)
 
 fun path_antiquotation binding check =
   antiquotation binding
     (Args.context -- Scan.lift (Parse.position Parse.path) >>
       (fn (ctxt, (name, pos)) => (check ctxt (SOME Path.current) (name, pos) |> Path.implode)))
     (fn {file_type, argument, ...} => #make_string file_type argument);
 
 val _ =
   Theory.setup
    (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
     path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
     path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
 
 end;