src/HOL/Tools/Predicate_Compile/predicate_compile.ML

       specialise = chk "specialise",
       fail_safe_function_flattening = false,
       no_topmost_reordering = (chk "no_topmost_reordering"),
       no_higher_order_predicate = [],
       inductify = chk "inductify",
+      detect_switches = chk "detect_switches",
       compilation = compilation
     }
   end
 
 fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy =