src/HOL/Tools/Nitpick/nitpick_isar.ML

    ("merge_type_vars", "false"),
    ("binary_ints", "smart"),
    ("destroy_constrs", "true"),
    ("specialize", "true"),
    ("star_linear_preds", "true"),
+   ("preconstr", "smart"),
    ("peephole_optim", "true"),
-   ("fix_datatype_vals", "true"),
    ("datatype_sym_break", "5"),
    ("kodkod_sym_break", "15"),
    ("timeout", "30"),
    ("tac_timeout", "0.5"),
    ("max_threads", "0"),

    ("dont_merge_type_vars", "merge_type_vars"),
    ("unary_ints", "binary_ints"),
    ("dont_destroy_constrs", "destroy_constrs"),
    ("dont_specialize", "specialize"),
    ("dont_star_linear_preds", "star_linear_preds"),
+   ("dont_preconstr", "preconstr"),
    ("no_peephole_optim", "peephole_optim"),
-   ("fix_datatype_vals", "dont_fix_datatype_vals"),
    ("no_debug", "debug"),
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("hide_datatypes", "show_datatypes"),
    ("hide_consts", "show_consts"),

    ("trust_genuine", "check_genuine")]
 
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) negated_params s orelse
-  member (op =) ["max", "show_all", "whack", "atoms", "eval", "expect"] s orelse
+  member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
          ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
-          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
-          "atoms"]
+          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr",
+          "dont_preconstr", "format", "atoms"]
 
 fun check_raw_param (s, _) =
   if is_known_raw_param s then ()
   else error ("Unknown parameter: " ^ quote s ^ ".")
 

     val merge_type_vars = lookup_bool "merge_type_vars"
     val binary_ints = lookup_bool_option "binary_ints"
     val destroy_constrs = lookup_bool "destroy_constrs"
     val specialize = lookup_bool "specialize"
     val star_linear_preds = lookup_bool "star_linear_preds"
+    val preconstrs =
+      lookup_bool_option_assigns read_term_polymorphic "preconstr"
     val peephole_optim = lookup_bool "peephole_optim"
-    val fix_datatype_vals = lookup_bool "fix_datatype_vals"
     val datatype_sym_break = lookup_int "datatype_sym_break"
     val kodkod_sym_break = lookup_int "kodkod_sym_break"
     val timeout = if auto then NONE else lookup_time "timeout"
     val tac_timeout = lookup_time "tac_timeout"
     val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
     val show_datatypes = debug orelse lookup_bool "show_datatypes"
     val show_consts = debug orelse lookup_bool "show_consts"
+    val evals = lookup_term_list_polymorphic "eval"
     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
     val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
-    val evals = lookup_term_list_polymorphic "eval"
     val max_potential =
       if auto then 0 else Int.max (0, lookup_int "max_potential")
     val max_genuine = Int.max (0, lookup_int "max_genuine")
     val check_potential = lookup_bool "check_potential"
     val check_genuine = lookup_bool "check_genuine"

      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
      debug = debug, verbose = verbose, overlord = overlord,
      user_axioms = user_axioms, assms = assms, whacks = whacks,
      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
      destroy_constrs = destroy_constrs, specialize = specialize,
-     star_linear_preds = star_linear_preds, peephole_optim = peephole_optim,
-     fix_datatype_vals = fix_datatype_vals,
-     datatype_sym_break = datatype_sym_break,
+     star_linear_preds = star_linear_preds, preconstrs = preconstrs,
+     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
      kodkod_sym_break = kodkod_sym_break, timeout = timeout,
      tac_timeout = tac_timeout, max_threads = max_threads,
      show_datatypes = show_datatypes, show_consts = show_consts,
-     formats = formats, atomss = atomss, evals = evals,
+     evals = evals, formats = formats, atomss = atomss,
      max_potential = max_potential, max_genuine = max_genuine,
      check_potential = check_potential, check_genuine = check_genuine,
      batch_size = batch_size, expect = expect}
   end