1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Feb 07 13:06:27 2018 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Feb 07 15:00:37 2018 +0100
     1.3 @@ -605,7 +605,7 @@
     1.4  if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n   matchsub (?a + (?b - ?c)) t_t |\n   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
     1.5  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
     1.6  show_types := false;*)
     1.7 -if term2str t = "~ (matchsub (?a + (?b + ?c)) t_t |\n   matchsub (?a + (?b - ?c)) t_t |\n" ^
     1.8 +if term2str t = "<not> (matchsub (?a + (?b + ?c)) t_t |\n   matchsub (?a + (?b - ?c)) t_t |\n" ^
     1.9  "   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
    1.10  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
    1.11