diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py
index 6ba3188a5633afff8eddd638d9f850600d095148..c2e518c12e737eb85f6cf59a8da34b8f8cb4b0b5 100755
--- a/tools/bitfield_gen.py
+++ b/tools/bitfield_gen.py
@@ -2505,6 +2505,9 @@ if __name__ == '__main__':
                 parser.error('Output file name must be given when generating HOL definitions or proofs')
             out_file.filename = os.path.abspath(options.thy_output_path)
 
+    if options.hol_proofs and not options.umm_types_file:
+        parser.error('--umm_types must be specified when generating HOL proofs')
+
     del parser
 
     options.output = out_file