src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML

 
 val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
 
 val options = 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,