nicer list of axioms used
authorpaulson
Thu Aug 18 13:09:40 2005 +0200 (2005-08-18)
changeset 17122278eb6251dc0
parent 17121 4c225f640b89
child 17123 c790951d0642
nicer list of axioms used
src/HOL/Tools/ATP/recon_transfer_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Aug 18 13:09:21 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Aug 18 13:09:40 2005 +0200
     1.3 @@ -305,9 +305,8 @@
     1.4  (*********************************************************************)
     1.5  
     1.6  
     1.7 -fun rules_to_string [] str = str
     1.8 -|   rules_to_string [x] str = str^x
     1.9 -|   rules_to_string (x::xs) str = rules_to_string xs (str^x^"   ")
    1.10 +fun rules_to_string [] = "NONE"
    1.11 +  | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
    1.12                                    
    1.13  
    1.14  val dummy_tac = PRIMITIVE(fn thm => thm );
    1.15 @@ -348,7 +347,8 @@
    1.16        (* produced from the clasimpset rather than the problem *)
    1.17  
    1.18        val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
    1.19 -      val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
    1.20 +      val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
    1.21 +                   rules_to_string axiom_names 
    1.22        val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
    1.23                           ("reconstring is: "^ax_str^"  "^goalstring)       
    1.24    in 
    1.25 @@ -389,7 +389,8 @@
    1.26      (***********************************)
    1.27  
    1.28       val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
    1.29 -     val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
    1.30 +     val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
    1.31 +                  rules_to_string axiom_names
    1.32      in 
    1.33  	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
    1.34           TextIO.output (toParent, ax_str^"\n");