src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

   val non_random_compilations : compilation list
   val random_compilations : compilation list
   (* Different options for compiler *)
   datatype options = Options of {  
     expected_modes : (string * mode list) option,
-    proposed_modes : (string * mode list) option,
+    proposed_modes : (string * mode list) list,
     proposed_names : ((string * mode) * string) list,
     show_steps : bool,
     show_proof_trace : bool,
     show_intermediate_results : bool,
     show_mode_inference : bool,

     inductify : bool,
     detect_switches : bool,
     compilation : compilation
   };
   val expected_modes : options -> (string * mode list) option
-  val proposed_modes : options -> (string * mode list) option
+  val proposed_modes : options -> string -> mode list option
   val proposed_names : options -> string -> mode -> string option
   val show_steps : options -> bool
   val show_proof_trace : options -> bool
   val show_intermediate_results : options -> bool
   val show_mode_inference : options -> bool

 
 (* Different options for compiler *)
 
 datatype options = Options of {  
   expected_modes : (string * mode list) option,
-  proposed_modes : (string * mode list) option,
+  proposed_modes : (string * mode list) list,
   proposed_names : ((string * mode) * string) list,
   show_steps : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
   show_mode_inference : bool,

   detect_switches : bool,
   compilation : compilation
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
-fun proposed_modes (Options opt) = #proposed_modes opt
+fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
 fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
   (#proposed_names opt) (name, mode)
 
 fun show_steps (Options opt) = #show_steps opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt

 
 fun detect_switches (Options opt) = #detect_switches opt
 
 val default_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,