371 | set_file_name NONE = I |
371 | set_file_name NONE = I |
372 val st' = |
372 val st' = |
373 st |
373 st |
374 |> Proof.map_context |
374 |> Proof.map_context |
375 (set_file_name dir |
375 (set_file_name dir |
376 #> (Option.map (Config.put ATP_Systems.e_selection_heuristic) |
376 #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) |
377 e_selection_heuristic |> the_default I) |
377 e_selection_heuristic |> the_default I) |
378 #> (Option.map (Config.put ATP_Systems.term_order) |
378 #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) |
379 term_order |> the_default I) |
379 term_order |> the_default I) |
380 #> (Option.map (Config.put ATP_Systems.force_sos) |
380 #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) |
381 force_sos |> the_default I)) |
381 force_sos |> the_default I)) |
382 val params as {max_facts, minimize, preplay_timeout, ...} = |
382 val params as {max_facts, minimize, preplay_timeout, ...} = |
383 Sledgehammer_Commands.default_params thy |
383 Sledgehammer_Commands.default_params thy |
384 ([(* ("verbose", "true"), *) |
384 ([(* ("verbose", "true"), *) |
385 ("fact_filter", fact_filter), |
385 ("fact_filter", fact_filter), |