1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 21 14:02:07 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 21 15:45:44 2011 +0100
     1.3 @@ -59,6 +59,7 @@
     1.4     ("specialize", "true"),
     1.5     ("star_linear_preds", "true"),
     1.6     ("peephole_optim", "true"),
     1.7 +   ("fix_datatype_vals", "true"),
     1.8     ("datatype_sym_break", "5"),
     1.9     ("kodkod_sym_break", "15"),
    1.10     ("timeout", "30"),
    1.11 @@ -91,6 +92,7 @@
    1.12     ("dont_specialize", "specialize"),
    1.13     ("dont_star_linear_preds", "star_linear_preds"),
    1.14     ("no_peephole_optim", "peephole_optim"),
    1.15 +   ("fix_datatype_vals", "dont_fix_datatype_vals"),
    1.16     ("no_debug", "debug"),
    1.17     ("quiet", "verbose"),
    1.18     ("no_overlord", "overlord"),
    1.19 @@ -252,6 +254,7 @@
    1.20      val specialize = lookup_bool "specialize"
    1.21      val star_linear_preds = lookup_bool "star_linear_preds"
    1.22      val peephole_optim = lookup_bool "peephole_optim"
    1.23 +    val fix_datatype_vals = lookup_bool "fix_datatype_vals"
    1.24      val datatype_sym_break = lookup_int "datatype_sym_break"
    1.25      val kodkod_sym_break = lookup_int "kodkod_sym_break"
    1.26      val timeout = if auto then NONE else lookup_time "timeout"
    1.27 @@ -282,6 +285,7 @@
    1.28       merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    1.29       destroy_constrs = destroy_constrs, specialize = specialize,
    1.30       star_linear_preds = star_linear_preds, peephole_optim = peephole_optim,
    1.31 +     fix_datatype_vals = fix_datatype_vals,
    1.32       datatype_sym_break = datatype_sym_break,
    1.33       kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    1.34       tac_timeout = tac_timeout, max_threads = max_threads,