diff -r a3d65f3b495f -r 4e6fc3336336 test/Tools/isac/Knowledge/polyeq-2.sml --- a/test/Tools/isac/Knowledge/polyeq-2.sml Tue Apr 21 16:16:11 2020 +0200 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Tue Apr 21 16:53:17 2020 +0200 @@ -256,9 +256,9 @@ (* the invisible parentheses are as expected *) val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0"; -trace_rewrite:=(*true*)false; +Trace.trace_rewrite:=(*true*)false; rewrite_set_ thy false expand_binoms t; -trace_rewrite:=false; +Trace.trace_rewrite:=false; "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";