src/HOL/Tools/res_atp.ML
changeset 21999 0cf192e489e2
parent 21980 d22f7e3c5ad9
child 22012 adf68479ae1b
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jan 04 17:52:28 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jan 04 17:55:12 2007 +0100
     1.3 @@ -823,13 +823,6 @@
     1.4    let val path = File.explode_platform_path fname
     1.5    in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
     1.6  
     1.7 -(*Converting a subgoal into negated conjecture clauses*)
     1.8 -fun neg_clauses th n =
     1.9 -  let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
    1.10 -      val st = Seq.hd (EVERY' tacs n th)
    1.11 -      val negs = Option.valOf (metahyps_thms n st)
    1.12 -  in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
    1.13 -
    1.14  (*We write out problem files for each subgoal. Argument probfile generates filenames,
    1.15    and allows the suppression of the suffix "_1" in problem-generation mode.
    1.16    FIXME: does not cope with &&, and it isn't easy because one could have multiple
    1.17 @@ -839,7 +832,8 @@
    1.18        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    1.19        val thy = ProofContext.theory_of ctxt
    1.20        fun get_neg_subgoals [] _ = []
    1.21 -        | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
    1.22 +        | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
    1.23 +                                         get_neg_subgoals gls (n+1)
    1.24        val goal_cls = get_neg_subgoals goals 1
    1.25        val logic = case !linkup_logic_mode of
    1.26                  Auto => problem_logic_goals (map ((map prop_of)) goal_cls)