# HG changeset patch
# User paulson
# Date 1138382951 -3600
# Node ID 8559cc115673049a10cf363a0e36b59e0ae28851
# Parent  5629fea8b4c668097d1ed1548772030bd9e911d2
tidying

diff -r 5629fea8b4c6 -r 8559cc115673 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- 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
diff -r 5629fea8b4c6 -r 8559cc115673 src/HOL/Tools/ATP/res_clasimpset.ML
--- 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;