src/HOL/Tools/Nitpick/nitpick_isar.ML

    ("assms", "true"),
    ("merge_type_vars", "false"),
    ("binary_ints", "smart"),
    ("destroy_constrs", "true"),
    ("specialize", "true"),
-   ("skolemize", "true"),
    ("star_linear_preds", "true"),
    ("fast_descrs", "true"),
    ("peephole_optim", "true"),
    ("timeout", "30 s"),
    ("tac_timeout", "500 ms"),

    ("no_assms", "assms"),
    ("dont_merge_type_vars", "merge_type_vars"),
    ("unary_ints", "binary_ints"),
    ("dont_destroy_constrs", "destroy_constrs"),
    ("dont_specialize", "specialize"),
-   ("dont_skolemize", "skolemize"),
    ("dont_star_linear_preds", "star_linear_preds"),
    ("full_descrs", "fast_descrs"),
    ("no_peephole_optim", "peephole_optim"),
    ("no_debug", "debug"),
    ("quiet", "verbose"),

     val assms = lookup_bool "assms"
     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 skolemize = lookup_bool "skolemize"
     val star_linear_preds = lookup_bool "star_linear_preds"
     val fast_descrs = lookup_bool "fast_descrs"
     val peephole_optim = lookup_bool "peephole_optim"
     val timeout = if auto then NONE else lookup_time "timeout"
     val tac_timeout = lookup_time "tac_timeout"

      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
      debug = debug, verbose = verbose, overlord = overlord,
      user_axioms = user_axioms, assms = assms,
      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
      destroy_constrs = destroy_constrs, specialize = specialize,
-     skolemize = skolemize, star_linear_preds = star_linear_preds,
-     fast_descrs = fast_descrs, peephole_optim = peephole_optim,
-     timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads,
+     star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+     peephole_optim = peephole_optim, timeout = timeout,
+     tac_timeout = tac_timeout, max_threads = max_threads,
      show_skolems = show_skolems, show_datatypes = show_datatypes,
      show_consts = show_consts, formats = formats, evals = evals,
      max_potential = max_potential, max_genuine = max_genuine,
      check_potential = check_potential, check_genuine = check_genuine,
      batch_size = batch_size, expect = expect}