src/HOL/Tools/res_axioms.ML
changeset 24042 968f42fe6836
parent 23592 ba0912262b2c
child 24137 8d7896398147
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Jul 29 14:29:57 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Jul 29 14:29:58 2007 +0200
     1.3 @@ -554,7 +554,7 @@
     1.4  fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
     1.5  fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
     1.6  
     1.7 -fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
     1.8 +fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
     1.9  
    1.10  
    1.11  (**** Translate a set of theorems into CNF ****)