src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 47129 e2e52c7d25c9
parent 46578 6bf7eec9b153
child 47148 0b8b73b49848
equal deleted inserted replaced
47128:6ded25a6098a 47129:e2e52c7d25c9
    71 val auto_minimize_max_time =
    71 val auto_minimize_max_time =
    72   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
    72   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
    73                            (K 5.0)
    73                            (K 5.0)
    74 
    74 
    75 fun adjust_reconstructor_params override_params
    75 fun adjust_reconstructor_params override_params
    76         ({debug, verbose, overlord, blocking, provers, type_enc, sound,
    76         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
    77          lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
    77          lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
    78          max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
    78          max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
    79          minimize, timeout, preplay_timeout, expect} : params) =
    79          minimize, timeout, preplay_timeout, expect} : params) =
    80   let
    80   let
    81     fun lookup_override name default_value =
    81     fun lookup_override name default_value =
    86        here. *)
    86        here. *)
    87     val type_enc = lookup_override "type_enc" type_enc
    87     val type_enc = lookup_override "type_enc" type_enc
    88     val lam_trans = lookup_override "lam_trans" lam_trans
    88     val lam_trans = lookup_override "lam_trans" lam_trans
    89   in
    89   in
    90     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    90     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    91      provers = provers, type_enc = type_enc, sound = sound,
    91      provers = provers, type_enc = type_enc, strict = strict,
    92      lam_trans = lam_trans, max_relevant = max_relevant,
    92      lam_trans = lam_trans, max_relevant = max_relevant,
    93      relevance_thresholds = relevance_thresholds,
    93      relevance_thresholds = relevance_thresholds,
    94      max_mono_iters = max_mono_iters,
    94      max_mono_iters = max_mono_iters,
    95      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    95      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    96      isar_shrink_factor = isar_shrink_factor, slice = slice,
    96      isar_shrink_factor = isar_shrink_factor, slice = slice,