src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 53053 6a3320758f0d
parent 53052 a0db255af8c5
child 53055 0fe8a9972eda
equal deleted inserted replaced
53052:a0db255af8c5 53053:6a3320758f0d
   501       SOME state =>
   501       SOME state =>
   502         let
   502         let
   503           val [provers_arg, timeout_arg, isar_proofs_arg] = args;
   503           val [provers_arg, timeout_arg, isar_proofs_arg] = args;
   504           val ctxt = Proof.context_of state
   504           val ctxt = Proof.context_of state
   505 
   505 
   506           val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
       
   507           val override_params =
   506           val override_params =
   508             ([("timeout", [timeout_arg]), ("blocking", ["true"])] @
   507             ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
   509             (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
   508               [("timeout", [timeout_arg]),
   510              then [("isar_proofs", [isar_proofs_arg])] else []) @
   509                ("isar_proofs", [isar_proofs_arg]),
   511             (if debug then [("debug", ["false"])] else []) @
   510                ("blocking", ["true"]),
   512             (if verbose then [("verbose", ["false"])] else []) @
   511                ("minimize", ["true"]),
   513             (if overlord then [("overlord", ["false"])] else []) @
   512                ("debug", ["false"]),
   514             (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]))
   513                ("verbose", ["false"]),
       
   514                ("overlord", ["false"])])
   515             |> map (normalize_raw_param ctxt)
   515             |> map (normalize_raw_param ctxt)
   516 
       
   517           val _ =
   516           val _ =
   518             run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
   517             run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
   519               no_fact_override (minimize_command override_params 1) state
   518               no_fact_override (minimize_command override_params 1) state
   520         in () end
   519         in () end
   521     | NONE => error "Unknown proof context"));
   520     | NONE => error "Unknown proof context"));