1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 16:16:11 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 16:53:17 2020 +0200
     1.3 @@ -49,8 +49,8 @@
     1.4  "----------- tests on predicates in problems ---------------------";
     1.5  "----------- tests on predicates in problems ---------------------";
     1.6  "----------- tests on predicates in problems ---------------------";
     1.7 -(* trace_rewrite:=true;
     1.8 - trace_rewrite:=false;
     1.9 +(* Trace.trace_rewrite:=true;
    1.10 + Trace.trace_rewrite:=false;
    1.11  *)
    1.12   val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
    1.13   val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
    1.14 @@ -160,7 +160,7 @@
    1.15    "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
    1.16  
    1.17    (*das rewriting l"asst sich beobachten mit
    1.18 -trace_rewrite := false;
    1.19 +Trace.trace_rewrite := false;
    1.20    *)
    1.21  
    1.22  "------15.11.02 --------------------------";
    1.23 @@ -168,7 +168,7 @@
    1.24    val bdv = (Thm.term_of o the o (parse thy)) "bdv";
    1.25    val a = (Thm.term_of o the o (parse thy)) "a";
    1.26   
    1.27 -trace_rewrite := false;
    1.28 +Trace.trace_rewrite := false;
    1.29   (* Anwenden einer Regelmenge aus Termorder.ML: *)
    1.30   val SOME (t,_) =
    1.31       rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;