# HG changeset patch
# User wenzelm
# Date 1159479770 -7200
# Node ID 8f947ffb5eb8078d149a29bfff5ac00ea348e13b
# Parent  468af396cf6f9254e57168dd87c4aae56fe44086
ResAtpset.get_atpset;

diff -r 468af396cf6f -r 8f947ffb5eb8 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Sep 28 23:42:49 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Sep 28 23:42:50 2006 +0200
@@ -567,13 +567,14 @@
 fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
 fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
 
-fun atpset_rules_of_thy thy = map pairname (ResAtpSet.atp_rules_of_thy thy);
+fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy));
 
 
 fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
 fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
 
-fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpSet.atp_rules_of_ctxt ctxt);
+fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt));
+
 
 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)