src/HOL/Tools/Predicate_Compile/code_prolog.ML

 
 (* values command *)
 
 val preprocess_options = Predicate_Compile_Aux.Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
   show_modes = false,
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = true,
   specialise = false,
   fail_safe_function_flattening = false,