# HG changeset patch
# User paulson
# Date 1124363380 -7200
# Node ID 278eb6251dc0675017e915c738c542a14bd03724
# Parent  4c225f640b890a8467c71ca75baffce05c1d2228
nicer list of axioms used

diff -r 4c225f640b89 -r 278eb6251dc0 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Aug 18 13:09:21 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Aug 18 13:09:40 2005 +0200
@@ -305,9 +305,8 @@
 (*********************************************************************)
 
 
-fun rules_to_string [] str = str
-|   rules_to_string [x] str = str^x
-|   rules_to_string (x::xs) str = rules_to_string xs (str^x^"   ")
+fun rules_to_string [] = "NONE"
+  | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
                                   
 
 val dummy_tac = PRIMITIVE(fn thm => thm );
@@ -348,7 +347,8 @@
       (* produced from the clasimpset rather than the problem *)
 
       val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
-      val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
+      val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
+                   rules_to_string axiom_names 
       val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
                          ("reconstring is: "^ax_str^"  "^goalstring)       
   in 
@@ -389,7 +389,8 @@
     (***********************************)
 
      val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
-     val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
+     val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
+                  rules_to_string axiom_names
     in 
 	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
          TextIO.output (toParent, ax_str^"\n");