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.
Changed some code due to changes in reduce_axiomsN.ML.
authormengj
Sat, 11 Feb 2006 14:25:23 +0100
changeset 19010 fef9e4881e83
parent 19009 bb29bf9d3a72
child 19011 d1c3294ca417
Changed some code due to changes in reduce_axiomsN.ML.
src/HOL/Tools/ATP/res_clasimpset.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Sat Feb 11 14:23:35 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Sat Feb 11 14:25:23 2006 +0100
@@ -252,7 +252,7 @@
  
       val cls_thms_list = make_unique (mk_clause_table 2200) 
                                       (List.concat (simpset_cls_thms@claset_cls_thms))
-      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
+      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
   in  (* create array of put clausename, number pairs into it *)
       (Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list))
   end;
isabelle