1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Feb 14 06:06:27 2018 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Feb 14 08:05:37 2018 +0100
     1.3 @@ -605,7 +605,10 @@
     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 = "<not> (matchsub (?a + (?b + ?c)) t_t |\n   matchsub (?a + (?b - ?c)) t_t |\n" ^
     1.8 -"   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
     1.9 +if term2str t =
    1.10 +  "\<not> (matchsub (?a + (?b + ?c)) t_t \<or>\n        " ^
    1.11 +  "matchsub (?a + (?b - ?c)) t_t \<or>\n        " ^
    1.12 +  "matchsub (?a - (?b + ?c)) t_t \<or> " ^
    1.13 +  "matchsub (?a + (?b - ?c)) t_t)"
    1.14  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
    1.15