src/HOL/TPTP/atp_problem_import.ML
changeset 47811 1e8eb643540d
parent 47794 4ad62c5f9f88
child 47812 bb477988edb4
     1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
     1.3 @@ -140,7 +140,8 @@
     1.4          ("overlord", if overlord then "true" else "false"),
     1.5          ("provers", prover),
     1.6          ("timeout", string_of_int timeout)] @ override_params)
     1.7 -      {add = [], del = [], only = true}
     1.8 +      {add = [(Facts.named (Thm.derivation_name ext), [])],
     1.9 +       del = [], only = true}
    1.10  
    1.11  fun sledgehammer_tac ctxt timeout i =
    1.12    let
    1.13 @@ -207,8 +208,8 @@
    1.14        read_tptp_file thy (freeze_problem_consts thy) file_name
    1.15      val conj = make_conj assms conjs
    1.16    in
    1.17 -    (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
    1.18 -     can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
    1.19 +    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
    1.20 +     can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
    1.21       can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
    1.22      |> print_szs_from_success conjs
    1.23    end