diff -r 4e6fc3336336 -r 07a042166900 test/Tools/isac/Knowledge/polyeq-1.sml
--- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 16:53:17 2020 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Apr 22 11:06:48 2020 +0200
@@ -49,8 +49,8 @@
 "----------- tests on predicates in problems ---------------------";
 "----------- tests on predicates in problems ---------------------";
 "----------- tests on predicates in problems ---------------------";
-(* Trace.trace_rewrite:=true;
- Trace.trace_rewrite:=false;
+(* Rewrite.trace_on:=true;
+ Rewrite.trace_on:=false;
 *)
  val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
@@ -160,7 +160,7 @@
   "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
 
   (*das rewriting l"asst sich beobachten mit
-Trace.trace_rewrite := false;
+Rewrite.trace_on := false;
   *)
 
 "------15.11.02 --------------------------";
@@ -168,7 +168,7 @@
   val bdv = (Thm.term_of o the o (parse thy)) "bdv";
   val a = (Thm.term_of o the o (parse thy)) "a";
  
-Trace.trace_rewrite := false;
+Rewrite.trace_on := false;
  (* Anwenden einer Regelmenge aus Termorder.ML: *)
  val SOME (t,_) =
      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;