src/HOL/Library/Old_SMT/old_smt_solver.ML
changeset 64304 96bc94c87a81
parent 62549 9498623b27f0
equal deleted inserted replaced
64303:605351c7ef97 64304:96bc94c87a81
    51 
    51 
    52 local
    52 local
    53 
    53 
    54 fun make_cmd command options problem_path proof_path =
    54 fun make_cmd command options problem_path proof_path =
    55   space_implode " "
    55   space_implode " "
    56     ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
    56     ("(exec 2>&1;" :: map Bash.string (command () @ options) @
    57       [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
    57       [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
    58 
    58 
    59 fun trace_and ctxt msg f x =
    59 fun trace_and ctxt msg f x =
    60   let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) ()
    60   let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) ()
    61   in f x end
    61   in f x end