ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML Mon Jan 23 11:38:43 2006 +0100
1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Mon Jan 23 11:41:54 2006 +0100
1.3 @@ -79,7 +79,7 @@
1.4 val relevant : int ref
1.5 val use_simpset: bool ref
1.6 val get_clasimp_lemmas :
1.7 - Proof.context -> term ->
1.8 + Proof.context -> term list ->
1.9 (ResClause.clause * thm) Array.array * ResClause.clause list
1.10 end;
1.11
1.12 @@ -317,15 +317,15 @@
1.13 (*Write out the claset and simpset rules of the supplied theory.
1.14 FIXME: argument "goal" is a hack to allow relevance filtering.
1.15 To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
1.16 -fun get_clasimp_lemmas ctxt goal =
1.17 +fun get_clasimp_lemmas ctxt goals =
1.18 let val claset_thms =
1.19 - map put_name_pair
1.20 - (ReduceAxiomsN.relevant_filter (!relevant) goal
1.21 + map put_name_pair (*FIXME: relevance filter should use ALL goals*)
1.22 + (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
1.23 (ResAxioms.claset_rules_of_ctxt ctxt))
1.24 val simpset_thms =
1.25 if !use_simpset then
1.26 map put_name_pair
1.27 - (ReduceAxiomsN.relevant_filter (!relevant) goal
1.28 + (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
1.29 (ResAxioms.simpset_rules_of_ctxt ctxt))
1.30 else []
1.31 val banned = make_banned_test (map #1 (claset_thms@simpset_thms))
2.1 --- a/src/HOL/Tools/res_atp.ML Mon Jan 23 11:38:43 2006 +0100
2.2 +++ b/src/HOL/Tools/res_atp.ML Mon Jan 23 11:41:54 2006 +0100
2.3 @@ -136,9 +136,8 @@
2.4 (*We write out problem files for each subgoal. Argument pf generates filenames,
2.5 and allows the suppression of the suffix "_1" in problem-generation mode.*)
2.6 fun write_problem_files pf (ctxt,th) =
2.7 - let val prems = Thm.prems_of th
2.8 - val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems)
2.9 - (*FIXME: hack!! need to consider relevance for all prems*)
2.10 + let val goals = Thm.prems_of th
2.11 + val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals
2.12 val _ = Output.debug ("claset and simprules total clauses = " ^
2.13 Int.toString (Array.length clause_arr))
2.14 val thy = ProofContext.theory_of ctxt
2.15 @@ -157,7 +156,7 @@
2.16 (axclauses,classrel_clauses,arity_clauses);
2.17 all_tac))]) n th;
2.18 pf n :: writenext (n-1))
2.19 - in (writenext (length prems), clause_arr) end;
2.20 + in (writenext (length goals), clause_arr) end;
2.21
2.22 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
2.23 Posix.Process.pid * string list) option);