src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 27 09:02:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -135,9 +135,10 @@
 datatype options = Options of {  
   expected_modes : (string * int list list) option,
   show_steps : bool,
-  show_mode_inference : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
+  show_mode_inference : bool,
+  show_modes : bool,
   show_compilation : bool,
   skip_proof : bool,
 
@@ -148,9 +149,10 @@
 
 fun expected_modes (Options opt) = #expected_modes opt
 fun show_steps (Options opt) = #show_steps opt
-fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
 fun show_proof_trace (Options opt) = #show_proof_trace opt
+fun show_modes (Options opt) = #show_modes opt
+fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_compilation (Options opt) = #show_compilation opt
 fun skip_proof (Options opt) = #skip_proof opt
 
@@ -163,6 +165,7 @@
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
+  show_modes = false,
   show_mode_inference = false,
   show_compilation = false,
   skip_proof = false,