| changeset 39383 | ddfafa97da2f | 
| parent 39382 | c797f3ab2ae1 | 
| child 40048 | f3a46d524101 | 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 15 09:36:38 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 15 09:36:39 2010 +0200 @@ -164,6 +164,7 @@ show_mode_inference = chk "show_mode_inference", show_compilation = chk "show_compilation", show_caught_failures = false, + show_invalid_clauses = chk "show_invalid_clauses", skip_proof = chk "skip_proof", function_flattening = not (chk "no_function_flattening"), specialise = chk "specialise",