# HG changeset patch
# User wenzelm
# Date 911999000 -3600
# Node ID 6cf4e46ce95ae10978b2f9781ea664c716a4e6ab
# Parent  2bebd0d0a961c175aa08794aa3cb29d03dc6dcf1
replaced prs by std_output / writeln;

diff -r 2bebd0d0a961 -r 6cf4e46ce95a src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Nov 25 14:01:08 1998 +0100
+++ b/src/Provers/blast.ML	Wed Nov 25 14:03:20 1998 +0100
@@ -632,6 +632,8 @@
   end;
 
 
+val prs = std_output;
+
 (*Print tracing information at each iteration of prover*)
 fun tracing sign brs = 
   let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
diff -r 2bebd0d0a961 -r 6cf4e46ce95a src/Provers/simp.ML
--- a/src/Provers/simp.ML	Wed Nov 25 14:01:08 1998 +0100
+++ b/src/Provers/simp.ML	Wed Nov 25 14:03:20 1998 +0100
@@ -380,11 +380,11 @@
 datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
 	       | PROVE | POP_CS | POP_ARTR | SPLIT;
 (*
-fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") |
-ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") |
-SIMP_LHS => prs("SIMP_LHS") | REW => prs("REW") | REFL => prs("REFL") |
-TRUE => prs("TRUE") | PROVE => prs("PROVE") | POP_CS => prs("POP_CS") | SPLIT
-=> prs("SPLIT");
+fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") |
+ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") |
+SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") |
+TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | SPLIT
+=> std_output("SPLIT");
 *)
 fun simp_refl([],_,ss) = ss
   | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)