src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17746 af59c748371d
parent 17718 9dab1e491d10
child 17772 818cec5f82a4
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Oct 04 09:58:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Oct 04 09:59:01 2005 +0200
     1.3 @@ -279,24 +279,19 @@
     1.4  fun rules_to_string [] = "NONE"
     1.5    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
     1.6  
     1.7 -fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
     1.8 -
     1.9 -val remove_linebreaks = subst_for #"\n" #"\t";
    1.10 -val restore_linebreaks = subst_for #"\t" #"\n";
    1.11 -
    1.12  
    1.13  fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
    1.14   let val _ = trace
    1.15                 ("\nGetting lemma names. proofstr is " ^ proofstr ^
    1.16 -                "\ngoalstr is " ^ goalstring ^
    1.17 -                "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
    1.18 +                "\ngoalstring is " ^ goalstring ^
    1.19 +                "num of clauses is " ^ string_of_int (Array.length clause_arr))
    1.20       val axiom_names = getax proofstr clause_arr
    1.21       val ax_str = rules_to_string axiom_names
    1.22      in 
    1.23  	 trace ("\nDone. Lemma list is " ^ ax_str);
    1.24           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    1.25                    ax_str ^ "\n");
    1.26 -	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    1.27 +	 TextIO.output (toParent, goalstring);
    1.28  	 TextIO.flushOut toParent;
    1.29  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    1.30      end
    1.31 @@ -304,8 +299,8 @@
    1.32       (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
    1.33               Toplevel.exn_message exn);
    1.34        TextIO.output (toParent, "Translation failed for the proof: " ^ 
    1.35 -                     remove_linebreaks proofstr ^ "\n");
    1.36 -      TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    1.37 +                     String.toString proofstr ^ "\n");
    1.38 +      TextIO.output (toParent, goalstring);
    1.39        TextIO.flushOut toParent;
    1.40        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.41  
    1.42 @@ -367,7 +362,7 @@
    1.43        val _ = trace ("\nReconstruction:\n" ^ reconstr)
    1.44    in 
    1.45         TextIO.output (toParent, reconstr^"\n");
    1.46 -       TextIO.output (toParent, goalstring^"\n");
    1.47 +       TextIO.output (toParent, goalstring);
    1.48         TextIO.flushOut toParent;
    1.49         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.50         all_tac
    1.51 @@ -375,8 +370,8 @@
    1.52    handle exn => (*FIXME: exn handler is too general!*)
    1.53     (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
    1.54      TextIO.output (toParent,"Translation failed for the proof:"^
    1.55 -         (remove_linebreaks proofstr) ^"\n");
    1.56 -    TextIO.output (toParent, goalstring^"\n");
    1.57 +         String.toString proofstr ^"\n");
    1.58 +    TextIO.output (toParent, goalstring);
    1.59      TextIO.flushOut toParent;
    1.60      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
    1.61  
    1.62 @@ -677,7 +672,8 @@
    1.63  
    1.64  fun apply_res_thm str goalstring  = 
    1.65    let val tokens = #1 (lex str);
    1.66 -      val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n")	
    1.67 +      val _ = trace ("\napply_res_thm. str is: "^str^
    1.68 +                     "\ngoalstring is: \n"^goalstring^"\n")	
    1.69        val (frees,recon_steps) = parse_step tokens 
    1.70    in 
    1.71        to_isar_proof (frees, recon_steps, goalstring)