src/HOL/Tools/ATP/res_clasimpset.ML
changeset 17484 f6a225f97f0a
parent 17412 e26cb20ef0cc
child 17525 ae5bb6001afb
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 19 14:20:45 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 19 15:12:13 2005 +0200
     1.3 @@ -112,8 +112,8 @@
     1.4    val use_simpset: bool ref
     1.5    val use_nameless: bool ref
     1.6    val get_clasimp_lemmas : 
     1.7 -         theory -> term -> 
     1.8 -         (ResClause.clause * thm) Array.array * int * ResClause.clause list 
     1.9 +         Proof.context -> term -> 
    1.10 +         (ResClause.clause * thm) Array.array * ResClause.clause list 
    1.11    end;
    1.12  
    1.13  structure ResClasimp : RES_CLASIMP =
    1.14 @@ -155,16 +155,16 @@
    1.15  (*Write out the claset and simpset rules of the supplied theory.
    1.16    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.17    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.18 -fun get_clasimp_lemmas thy goal = 
    1.19 +fun get_clasimp_lemmas ctxt goal = 
    1.20      let val claset_rules = 
    1.21                map put_name_pair
    1.22  	        (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.23 -		  (ResAxioms.claset_rules_of_thy thy));
    1.24 +		  (ResAxioms.claset_rules_of_ctxt ctxt));
    1.25  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []);
    1.26  
    1.27  	val simpset_rules =
    1.28  	      ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.29 -                (ResAxioms.simpset_rules_of_thy thy);
    1.30 +                (ResAxioms.simpset_rules_of_ctxt ctxt);
    1.31  	val named_simpset = map put_name_pair simpset_rules
    1.32  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.33  
    1.34 @@ -184,7 +184,7 @@
    1.35  	(*********************************************************)
    1.36  	val clause_arr = Array.fromList whole_list;
    1.37    in
    1.38 -	(clause_arr, List.length whole_list, clauses)
    1.39 +	(clause_arr, clauses)
    1.40    end;
    1.41  
    1.42