src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML

 
 datatype options = Options of {  
   (*check_modes : (string * int list list) list,*)
   show_steps : bool,
   show_mode_inference : bool,
+  show_proof_trace : bool,
   show_intermediate_results : bool,
   (*
   inductify_functions : bool,
   *)
   inductify : bool,
   rpred : bool
 };
 
 fun show_steps (Options opt) = #show_steps opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
+fun show_proof_trace (Options opt) = #show_proof_trace 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_proof_trace = false,
   show_mode_inference = false,
   inductify = false,
   rpred = false
 }