Changed some code due to changes in reduce_axiomsN.ML.
authormengj
Sat Feb 11 14:25:23 2006 +0100 (2006-02-11)
changeset 19010fef9e4881e83
parent 19009 bb29bf9d3a72
child 19011 d1c3294ca417
Changed some code due to changes in reduce_axiomsN.ML.
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Sat Feb 11 14:23:35 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Sat Feb 11 14:25:23 2006 +0100
     1.3 @@ -252,7 +252,7 @@
     1.4   
     1.5        val cls_thms_list = make_unique (mk_clause_table 2200) 
     1.6                                        (List.concat (simpset_cls_thms@claset_cls_thms))
     1.7 -      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
     1.8 +      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
     1.9    in  (* create array of put clausename, number pairs into it *)
    1.10        (Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list))
    1.11    end;