replaced prs by std_output / writeln;
authorwenzelm
Wed Nov 25 14:03:20 1998 +0100 (1998-11-25 ago)
changeset 59616cf4e46ce95a
parent 5960 2bebd0d0a961
child 5962 0f7375e5e977
replaced prs by std_output / writeln;
src/Provers/blast.ML
src/Provers/simp.ML
     1.1 --- a/src/Provers/blast.ML	Wed Nov 25 14:01:08 1998 +0100
     1.2 +++ b/src/Provers/blast.ML	Wed Nov 25 14:03:20 1998 +0100
     1.3 @@ -632,6 +632,8 @@
     1.4    end;
     1.5  
     1.6  
     1.7 +val prs = std_output;
     1.8 +
     1.9  (*Print tracing information at each iteration of prover*)
    1.10  fun tracing sign brs = 
    1.11    let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
     2.1 --- a/src/Provers/simp.ML	Wed Nov 25 14:01:08 1998 +0100
     2.2 +++ b/src/Provers/simp.ML	Wed Nov 25 14:03:20 1998 +0100
     2.3 @@ -380,11 +380,11 @@
     2.4  datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
     2.5  	       | PROVE | POP_CS | POP_ARTR | SPLIT;
     2.6  (*
     2.7 -fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") |
     2.8 -ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") |
     2.9 -SIMP_LHS => prs("SIMP_LHS") | REW => prs("REW") | REFL => prs("REFL") |
    2.10 -TRUE => prs("TRUE") | PROVE => prs("PROVE") | POP_CS => prs("POP_CS") | SPLIT
    2.11 -=> prs("SPLIT");
    2.12 +fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") |
    2.13 +ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") |
    2.14 +SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") |
    2.15 +TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | SPLIT
    2.16 +=> std_output("SPLIT");
    2.17  *)
    2.18  fun simp_refl([],_,ss) = ss
    2.19    | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)