--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Jan 27 18:28:55 2006 +0100
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Jan 27 18:29:11 2006 +0100
@@ -268,7 +268,7 @@
(*The signal handler in watcher.ML must be able to read the output of this.*)
fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr =
let val _ = trace
- ("\nGetting lemma names. proofstr is " ^ proofstr ^
+ ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
"\nprobfile is " ^ probfile ^
" num of clauses is " ^ string_of_int (Array.length clause_arr))
val axiom_names = getax proofstr clause_arr
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Fri Jan 27 18:28:55 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Jan 27 18:29:11 2006 +0100
@@ -260,20 +260,19 @@
val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
-
- val cls_thms_list = make_unique (mk_clause_table 2200)
+ val cls_thms_list = make_unique (mk_clause_table 2200)
(List.concat (simpset_cls_thms@claset_cls_thms))
-
- val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
+ val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
(* Identify the set of clauses to be written out *)
- val clauses = map #1(relevant_cls_thms_list);
+ val clauses = map #1 (relevant_cls_thms_list);
val cls_nums = map ResClause.num_of_clauses clauses;
(*Note: in every case, cls_num = 1. I think that only conjecture clauses
can have any other value.*)
val whole_list = List.concat
(map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums)));
-
in (* create array of put clausename, number pairs into it *)
+ assert (map #1 whole_list = clauses) "get_clasimp_lemmas";
+ (*So get rid of cls_nums and clause_numbering; return simply cls_thms_list*)
(Array.fromList whole_list, clauses)
end;