src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39383 ddfafa97da2f
parent 39382 c797f3ab2ae1
child 39541 6605c1e87c7f
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:38 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:39 2010 +0200
     1.3 @@ -108,6 +108,7 @@
     1.4      show_modes : bool,
     1.5      show_compilation : bool,
     1.6      show_caught_failures : bool,
     1.7 +    show_invalid_clauses : bool,
     1.8      skip_proof : bool,
     1.9      no_topmost_reordering : bool,
    1.10      function_flattening : bool,
    1.11 @@ -128,6 +129,7 @@
    1.12    val show_modes : options -> bool
    1.13    val show_compilation : options -> bool
    1.14    val show_caught_failures : options -> bool
    1.15 +  val show_invalid_clauses : options -> bool
    1.16    val skip_proof : options -> bool
    1.17    val no_topmost_reordering : options -> bool
    1.18    val function_flattening : options -> bool
    1.19 @@ -712,6 +714,7 @@
    1.20    show_modes : bool,
    1.21    show_compilation : bool,
    1.22    show_caught_failures : bool,
    1.23 +  show_invalid_clauses : bool,
    1.24    skip_proof : bool,
    1.25    no_topmost_reordering : bool,
    1.26    function_flattening : bool,
    1.27 @@ -735,7 +738,7 @@
    1.28  fun show_mode_inference (Options opt) = #show_mode_inference opt
    1.29  fun show_compilation (Options opt) = #show_compilation opt
    1.30  fun show_caught_failures (Options opt) = #show_caught_failures opt
    1.31 -
    1.32 +fun show_invalid_clauses (Options opt) = #show_invalid_clauses opt
    1.33  fun skip_proof (Options opt) = #skip_proof opt
    1.34  
    1.35  fun function_flattening (Options opt) = #function_flattening opt
    1.36 @@ -761,6 +764,7 @@
    1.37    show_mode_inference = false,
    1.38    show_compilation = false,
    1.39    show_caught_failures = false,
    1.40 +  show_invalid_clauses = false,
    1.41    skip_proof = true,
    1.42    no_topmost_reordering = false,
    1.43    function_flattening = false,
    1.44 @@ -773,8 +777,8 @@
    1.45  }
    1.46  
    1.47  val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
    1.48 -  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
    1.49 -  "detect_switches", "specialise", "no_topmost_reordering"]
    1.50 +  "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
    1.51 +  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering"]
    1.52  
    1.53  fun print_step options s =
    1.54    if show_steps options then tracing s else ()