+let generate_theory theory_file deps =
+ if theory_file = "" then deps else
+ let map (files, deps) (t, d) =
+ if t = theory_file then files, deps else
+ S.add t files, List.fold_left (fun deps dep -> S.add dep deps) deps d
+ in
+ let out_include och dep =
+ Printf.fprintf och "include \"%s\".\n\n" dep
+ in
+ let fileset, depset = List.fold_left map (S.empty, S.empty) deps in
+ let top_depset = S.diff fileset depset in
+ let och = open_out theory_file in
+ begin
+ MatitaMisc.out_preamble och;
+ S.iter (out_include och) top_depset;
+ close_out och;
+ (theory_file, S.elements top_depset) :: deps
+ end
+