--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 09:02:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 09:03:56 2009 +0100
@@ -114,6 +114,7 @@
show_steps = chk "show_steps",
show_intermediate_results = chk "show_intermediate_results",
show_proof_trace = chk "show_proof_trace",
+ show_modes = chk "show_modes",
show_mode_inference = chk "show_mode_inference",
show_compilation = chk "show_compilation",
skip_proof = chk "skip_proof",
@@ -146,7 +147,7 @@
val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
-val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
+val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"]
local structure P = OuterParse