--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200
@@ -112,7 +112,7 @@
(*check_modes : (string * int list list) list,*)
show_steps : bool,
show_mode_inference : bool,
-
+ show_intermediate_results : bool,
(*
inductify_functions : bool,
*)
@@ -120,13 +120,16 @@
rpred : bool
};
-fun is_show_steps (Options opt) = #show_steps opt
+fun show_steps (Options opt) = #show_steps opt
+fun show_intermediate_results (Options opt) = #show_intermediate_results opt
+
fun is_inductify (Options opt) = #inductify opt
fun is_rpred (Options opt) = #rpred opt
val default_options = Options {
show_steps = false,
+ show_intermediate_results = false,
show_mode_inference = false,
inductify = false,
rpred = false
@@ -134,7 +137,7 @@
fun print_step options s =
- if is_show_steps options then tracing s else ()
+ if show_steps options then tracing s else ()
(* tuple processing *)