diff -r 36aeb535a801 -r 6de8b7a5cd44 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Mar 29 13:48:10 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Mar 29 16:53:46 2019 +0100
@@ -10,6 +10,7 @@
   val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
   val write_files: theory -> Path.T -> (Path.T * Position.T) list
   val export_files: theory -> theory list -> (Path.T * Position.T) list
+  val the_file_content: theory -> Path.T -> string
   type file_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
@@ -84,6 +85,13 @@
     get_files other_thy |> map (fn {path, pos, content} =>
       (Export.export thy path [content]; (path, pos))));
 
+fun the_file_content thy path =
+  (case find_first (fn file => #path file = path) (get_files thy) of
+    SOME {content, ...} => content
+  | NONE =>
+      error ("Missing generated file " ^ Path.print path ^
+        " in theory " ^ quote (Context.theory_long_name thy)));
+
 
 (* file types *)