src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 50824 a991d603aac6
parent 50823 0583db803066
child 51130 76d68444cd59
equal deleted inserted replaced
50823:0583db803066 50824:a991d603aac6
   371 
   371 
   372 val default_learn_prover_timeout = 2.0
   372 val default_learn_prover_timeout = 2.0
   373 
   373 
   374 fun hammer_away override_params subcommand opt_i fact_override state =
   374 fun hammer_away override_params subcommand opt_i fact_override state =
   375   let
   375   let
   376     (* this is necessary to avoid errors in jedit *)
   376     (* necessary to avoid problems in jedit *)
   377     val state = state |> Proof.map_context (Config.put show_markup false)
   377     val state = state |> Proof.map_context (Config.put show_markup false)
   378     val ctxt = Proof.context_of state
   378     val ctxt = Proof.context_of state
   379     val override_params = override_params |> map (normalize_raw_param ctxt)
   379     val override_params = override_params |> map (normalize_raw_param ctxt)
   380     val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
   380     val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
   381   in
   381   in