src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39382 c797f3ab2ae1
parent 39312 968c33be5c96
child 39383 ddfafa97da2f
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 08:58:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:38 2010 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    (* Different options for compiler *)
     1.5    datatype options = Options of {  
     1.6      expected_modes : (string * mode list) option,
     1.7 -    proposed_modes : (string * mode list) option,
     1.8 +    proposed_modes : (string * mode list) list,
     1.9      proposed_names : ((string * mode) * string) list,
    1.10      show_steps : bool,
    1.11      show_proof_trace : bool,
    1.12 @@ -119,7 +119,7 @@
    1.13      compilation : compilation
    1.14    };
    1.15    val expected_modes : options -> (string * mode list) option
    1.16 -  val proposed_modes : options -> (string * mode list) option
    1.17 +  val proposed_modes : options -> string -> mode list option
    1.18    val proposed_names : options -> string -> mode -> string option
    1.19    val show_steps : options -> bool
    1.20    val show_proof_trace : options -> bool
    1.21 @@ -703,7 +703,7 @@
    1.22  
    1.23  datatype options = Options of {  
    1.24    expected_modes : (string * mode list) option,
    1.25 -  proposed_modes : (string * mode list) option,
    1.26 +  proposed_modes : (string * mode list) list,
    1.27    proposed_names : ((string * mode) * string) list,
    1.28    show_steps : bool,
    1.29    show_proof_trace : bool,
    1.30 @@ -724,7 +724,7 @@
    1.31  };
    1.32  
    1.33  fun expected_modes (Options opt) = #expected_modes opt
    1.34 -fun proposed_modes (Options opt) = #proposed_modes opt
    1.35 +fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
    1.36  fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
    1.37    (#proposed_names opt) (name, mode)
    1.38  
    1.39 @@ -752,7 +752,7 @@
    1.40  
    1.41  val default_options = Options {
    1.42    expected_modes = NONE,
    1.43 -  proposed_modes = NONE,
    1.44 +  proposed_modes = [],
    1.45    proposed_names = [],
    1.46    show_steps = false,
    1.47    show_intermediate_results = false,