src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 41206 b16fbb148a16
parent 41155 85da8cbb4966
child 41210 15fbf30288e1
equal deleted inserted replaced
41205:209546e0af2c 41206:b16fbb148a16
   344   SH_ERROR
   344   SH_ERROR
   345 
   345 
   346 fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
   346 fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
   347   let
   347   let
   348     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
   348     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
   349     val thy = ProofContext.theory_of ctxt
       
   350     val i = 1
   349     val i = 1
   351     fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir
   350     fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir
   352       | change_dir NONE = I
   351       | change_dir NONE = I
   353     val st' =
   352     val st' =
   354       st |> Proof.map_context
   353       st |> Proof.map_context
   536     let
   535     let
   537       val reconstructor = Unsynchronized.ref ""
   536       val reconstructor = Unsynchronized.ref ""
   538       val named_thms =
   537       val named_thms =
   539         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
   538         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
   540       val ctxt = Proof.context_of pre
   539       val ctxt = Proof.context_of pre
   541       val (prover_name, _) = get_prover ctxt args
       
   542       val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
       
   543       val minimize = AList.defined (op =) args minimizeK
   540       val minimize = AList.defined (op =) args minimizeK
   544       val metis_ft = AList.defined (op =) args metis_ftK
   541       val metis_ft = AList.defined (op =) args metis_ftK
   545       val trivial =
   542       val trivial =
   546        TimeLimit.timeLimit try_outer_timeout
   543        TimeLimit.timeLimit try_outer_timeout
   547                                    (Try.invoke_try (SOME try_inner_timeout)) pre
   544                                    (Try.invoke_try (SOME try_inner_timeout)) pre