# HG changeset patch
# User wenzelm
# Date 1185712198 -7200
# Node ID 968f42fe68367fee780b011bf2ab9319a86de6aa
# Parent  d5845b7c1a240d3b42b13724b66c5cec87ddf57f
simplified ResAtpset via NamedThmsFun;

diff -r d5845b7c1a24 -r 968f42fe6836 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Jul 29 14:29:57 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sun Jul 29 14:29:58 2007 +0200
@@ -554,7 +554,7 @@
 fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
 fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
 
-fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
+fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
 
 
 (**** Translate a set of theorems into CNF ****)