tidying
authorpaulson
Fri Jan 27 18:29:11 2006 +0100 (2006-01-27)
changeset 187978559cc115673
parent 18796 5629fea8b4c6
child 18798 ca02a2077955
tidying
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Jan 27 18:28:55 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Jan 27 18:29:11 2006 +0100
     1.3 @@ -268,7 +268,7 @@
     1.4  (*The signal handler in watcher.ML must be able to read the output of this.*)
     1.5  fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
     1.6   let val _ = trace
     1.7 -               ("\nGetting lemma names. proofstr is " ^ proofstr ^
     1.8 +               ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
     1.9                  "\nprobfile is " ^ probfile ^
    1.10                  "  num of clauses is " ^ string_of_int (Array.length clause_arr))
    1.11       val axiom_names = getax proofstr clause_arr
     2.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 18:28:55 2006 +0100
     2.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 18:29:11 2006 +0100
     2.3 @@ -260,20 +260,19 @@
     2.4        val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
     2.5        val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
     2.6   
     2.7 -
     2.8 -     val cls_thms_list = make_unique (mk_clause_table 2200) 
     2.9 +      val cls_thms_list = make_unique (mk_clause_table 2200) 
    2.10                                        (List.concat (simpset_cls_thms@claset_cls_thms))
    2.11 -
    2.12 -     val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
    2.13 +      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
    2.14        (* Identify the set of clauses to be written out *)
    2.15 -      val clauses = map #1(relevant_cls_thms_list);
    2.16 +      val clauses = map #1 (relevant_cls_thms_list);
    2.17        val cls_nums = map ResClause.num_of_clauses clauses;
    2.18        (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
    2.19  	can have any other value.*)
    2.20        val whole_list = List.concat 
    2.21  	    (map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums)));
    2.22 -      
    2.23    in  (* create array of put clausename, number pairs into it *)
    2.24 +      assert (map #1 whole_list = clauses) "get_clasimp_lemmas";
    2.25 +      (*So get rid of cls_nums and clause_numbering; return simply cls_thms_list*)
    2.26        (Array.fromList whole_list, clauses)
    2.27    end;
    2.28