src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML

   expected_modes : (string * int list list) option,
   show_steps : bool,
   show_mode_inference : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
+  show_compilation : bool,
+  skip_proof : bool,
 
   inductify : bool,
   rpred : bool,
   depth_limited : bool
 };

 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_compilation (Options opt) = #show_compilation opt
+fun skip_proof (Options opt) = #skip_proof opt
 
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt
 fun is_depth_limited (Options opt) = #depth_limited opt
 

   expected_modes = NONE,
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
   show_mode_inference = false,
+  show_compilation = false,
+  skip_proof = false,
+  
   inductify = false,
   rpred = false,
   depth_limited = false
 }
 
 
 fun print_step options s =
   if show_steps options then tracing s else ()
-
 
 (* tuple processing *)
 
 fun expand_tuples thy intro =
   let