src/HOL/Tools/res_atp.ML
changeset 21506 b2a673894ce5
parent 21470 7c1b59ddcd56
child 21509 6c5755ad9cae
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Nov 23 22:38:29 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Nov 23 22:38:30 2006 +0100
     1.3 @@ -581,13 +581,13 @@
     1.4  	          (name_thm_pairs ctxt))
     1.5  	else 
     1.6  	let val claset_thms =
     1.7 -		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
     1.8 +		if !include_claset then ResAxioms.claset_rules_of ctxt
     1.9  		else []
    1.10  	    val simpset_thms = 
    1.11 -		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
    1.12 +		if !include_simpset then ResAxioms.simpset_rules_of ctxt
    1.13  		else []
    1.14  	    val atpset_thms =
    1.15 -		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
    1.16 +		if !include_atpset then ResAxioms.atpset_rules_of ctxt
    1.17  		else []
    1.18  	    val _ = if !Output.show_debug_msgs 
    1.19  		    then (Output.debug "ATP theorems: "; display_thms atpset_thms)