src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 41338 ffd730fcf0ac
parent 41337 263fe1670067
child 41357 ae76960d86a2
equal deleted inserted replaced
41337:263fe1670067 41338:ffd730fcf0ac
   348     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
   348     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
   349     val i = 1
   349     val i = 1
   350     fun change_dir (SOME dir) =
   350     fun change_dir (SOME dir) =
   351         Config.put Sledgehammer_Provers.dest_dir dir
   351         Config.put Sledgehammer_Provers.dest_dir dir
   352         #> Config.put SMT_Config.debug_files
   352         #> Config.put SMT_Config.debug_files
   353           (dir ^ "/" ^ ATP_Problem.timestamp () ^ "_" ^ serial_string ())
   353           (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_"
       
   354           ^ serial_string ())
   354       | change_dir NONE = I
   355       | change_dir NONE = I
   355     val st' =
   356     val st' =
   356       st |> Proof.map_context
   357       st |> Proof.map_context
   357                 (change_dir dir
   358                 (change_dir dir
   358                  #> Config.put Sledgehammer_Provers.measure_run_time true)
   359                  #> Config.put Sledgehammer_Provers.measure_run_time true)