--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 15 09:36:38 2010 +0200
@@ -99,7 +99,7 @@
(* 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,
@@ -119,7 +119,7 @@
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
@@ -703,7 +703,7 @@
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,
@@ -724,7 +724,7 @@
};
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)
@@ -752,7 +752,7 @@
val default_options = Options {
expected_modes = NONE,
- proposed_modes = NONE,
+ proposed_modes = [],
proposed_names = [],
show_steps = false,
show_intermediate_results = false,