1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Jul 16 07:45:06 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Sat Jul 17 14:05:28 2021 +0200
     1.3 @@ -319,10 +319,10 @@
     1.4  "----------- build verschoenere ----------------------------------";
     1.5  "----------- build verschoenere ----------------------------------";
     1.6  "----------- build verschoenere ----------------------------------";
     1.7 -val t = TermC.str2term "3 + -2 * e + 2 * f + 2 * g";
     1.8 +val t = TermC.str2term "3 + - 2 * e + 2 * f + 2 * g";
     1.9  val SOME (t,_) = rewrite_set_ thy false verschoenere t;
    1.10  if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
    1.11 -else error "polyminus.sml: verschoenere 3 + -2 * e ...";
    1.12 +else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
    1.13  
    1.14  (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
    1.15  Rewrite.trace_on:=false;