Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Goals in clause form are sent to the relevance filter.
authormengj
Mon, 27 Nov 2006 23:47:42 +0100
changeset 21563 b4718f2c15f0
parent 21562 dd39c9e62f19
child 21564 519ee3129ee1
Goals in clause form are sent to the relevance filter.
src/HOL/Tools/res_atp.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_atp.ML	Mon Nov 27 21:07:00 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Mon Nov 27 23:47:42 2006 +0100
@@ -863,8 +863,7 @@
       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
       val white_cls = ResAxioms.cnf_rules_pairs white_thms
       (*clauses relevant to goal gl*)
-      val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
-                           goals
+      val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
                   axcls_list
       val keep_types = if is_fol_logic logic then !ResClause.keep_types
isabelle