1.1 --- a/test/Tools/isac/Knowledge/atools.sml	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/atools.sml	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4  if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () 
     1.5  else error "atools.sml diff.behav. in eval_boollist2sum";
     1.6  
     1.7 -trace_rewrite:=true;
     1.8 +trace_rewrite := false;
     1.9  val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls 
    1.10  		      [Calc ("Atools.boollist2sum", eval_boollist2sum "")];
    1.11  val t = str2t 
    1.12 @@ -238,7 +238,7 @@
    1.13    "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
    1.14  
    1.15    (*das rewriting l"asst sich beobachten mit
    1.16 -  trace_rewrite:=true;
    1.17 +trace_rewrite := false;
    1.18    *)
    1.19  
    1.20  "------15.11.02 --------------------------";
    1.21 @@ -246,7 +246,7 @@
    1.22    val bdv = (term_of o the o (parse thy)) "bdv";
    1.23    val a = (term_of o the o (parse thy)) "a";
    1.24   
    1.25 - trace_rewrite:=true;
    1.26 +trace_rewrite := false;
    1.27   (* Anwenden einer Regelmenge aus Termorder.ML: *)
    1.28   val SOME (t,_) =
    1.29       rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;