src/HOL/Tools/ATP/res_clasimpset.ML
changeset 18797 8559cc115673
parent 18792 fb427f4a01f2
child 18869 00741f7280f7
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 18:28:55 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 18:29:11 2006 +0100
     1.3 @@ -260,20 +260,19 @@
     1.4        val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
     1.5        val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
     1.6   
     1.7 -
     1.8 -     val cls_thms_list = make_unique (mk_clause_table 2200) 
     1.9 +      val cls_thms_list = make_unique (mk_clause_table 2200) 
    1.10                                        (List.concat (simpset_cls_thms@claset_cls_thms))
    1.11 -
    1.12 -     val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
    1.13 +      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
    1.14        (* Identify the set of clauses to be written out *)
    1.15 -      val clauses = map #1(relevant_cls_thms_list);
    1.16 +      val clauses = map #1 (relevant_cls_thms_list);
    1.17        val cls_nums = map ResClause.num_of_clauses clauses;
    1.18        (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
    1.19  	can have any other value.*)
    1.20        val whole_list = List.concat 
    1.21  	    (map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums)));
    1.22 -      
    1.23    in  (* create array of put clausename, number pairs into it *)
    1.24 +      assert (map #1 whole_list = clauses) "get_clasimp_lemmas";
    1.25 +      (*So get rid of cls_nums and clause_numbering; return simply cls_thms_list*)
    1.26        (Array.fromList whole_list, clauses)
    1.27    end;
    1.28