src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 39383 ddfafa97da2f
parent 39187 1d26c4006c14
child 39461 0ed0f015d140
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 15 09:36:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 15 09:36:39 2010 +0200
@@ -676,7 +676,7 @@
 
 val preprocess_options = Predicate_Compile_Aux.Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
@@ -685,6 +685,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = true,