# HG changeset patch
# User mengj
# Date 1139664323 -3600
# Node ID fef9e4881e833bb1198ce469c893d45ac047d45f
# Parent  bb29bf9d3a725d93f81ed471074ed5b5caac84dc
Changed some code due to changes in reduce_axiomsN.ML.

diff -r bb29bf9d3a72 -r fef9e4881e83 src/HOL/Tools/ATP/res_clasimpset.ML
--- 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;