src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19010 fef9e4881e83
parent 18985 bc23b1d1ddea
child 19156 bdaa8a980431
     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;