src/HOL/Tools/ATP/res_clasimpset.ML
changeset 16897 7e5319d0f418
parent 16795 b400b53d8f7d
child 16906 74eddde1de2f
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jul 20 15:57:10 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jul 20 17:00:28 2005 +0200
     1.3 @@ -185,7 +185,6 @@
     1.4                ReduceAxiomsN.relevant_filter (!relevant) goal 
     1.5                  (ResAxioms.claset_rules_of_thy thy);
     1.6  	val named_claset = List.filter has_name_pair claset_rules;
     1.7 -	val claset_names = map remove_spaces_pair (named_claset)
     1.8  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
     1.9  
    1.10  	val simpset_rules =