Now ResHolClause also does first-order problems!
authorpaulson
Thu Jun 14 13:19:50 2007 +0200 (2007-06-14)
changeset 233877cb8faa5d4d3
parent 23386 9255c1a75ba9
child 23388 77645da0db85
Now ResHolClause also does first-order problems!
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jun 14 13:18:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jun 14 13:19:50 2007 +0200
     1.3 @@ -691,15 +691,9 @@
     1.4    likely to lead to unsound proofs.*)
     1.5  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
     1.6  
     1.7 -fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
     1.8 -    if is_fol_logic logic
     1.9 -    then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
    1.10 -    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
    1.11 +fun tptp_writer logic = ResHolClause.tptp_write_file (logic=FOL);
    1.12  
    1.13 -fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
    1.14 -    if is_fol_logic logic
    1.15 -    then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
    1.16 -    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
    1.17 +fun dfg_writer logic = ResHolClause.dfg_write_file (logic=FOL);
    1.18  
    1.19  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
    1.20  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
    1.21 @@ -819,7 +813,7 @@
    1.22                                           get_neg_subgoals gls (n+1)
    1.23        val goal_cls = get_neg_subgoals goals 1
    1.24        val logic = case !linkup_logic_mode of
    1.25 -                Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
    1.26 +                Auto => problem_logic_goals (map (map prop_of) goal_cls)
    1.27                | Fol => FOL
    1.28                | Hol => HOL
    1.29        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []