1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Wed Aug 28 10:40:53 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Wed Aug 28 11:02:03 2013 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4  val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
     1.5  val SOME (t', asm) = factout_p_ thy t;
     1.6  if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso 
     1.7 -  terms2str asm = "[\"2 ~= 0\",\"1 + x ~= 0\"]"
     1.8 +  terms2str asm = "[\"1 + x ~= 0\"]"
     1.9  then () else error "factout_p_ 1 changed";
    1.10  
    1.11  "-------- fun cancel_p_ ------------------------------------------------------";
    1.12 @@ -132,7 +132,7 @@
    1.13  "-------- fun cancel_p_ ------------------------------------------------------";
    1.14  val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
    1.15  val SOME (t', asm) = cancel_p_ thy t;
    1.16 -if (term2str t', terms2str asm) = ("(x + y) / x", "[\"x ~= 0\",\"x + -1 * y ~= 0\"]")
    1.17 +if (term2str t', terms2str asm) = ("(x + y) / x", "[\"x ~= 0\"]")
    1.18  then () else error ("cancel_p_ (t', asm) 1 changed: " ^ term2str t')
    1.19  ;
    1.20  val t = str2term "nothing + to_cancel ::real";
    1.21 @@ -140,7 +140,7 @@
    1.22  ;
    1.23  val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
    1.24  val SOME (t', asm) = cancel_p_ thy t;
    1.25 -if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"2 ~= 0\",\"1 + x ~= 0\"]"
    1.26 +if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[]"
    1.27  then () else error "cancel_p_ 1 changed";
    1.28  
    1.29  "-------- fun common_nominator_p_ --------------------------------------------";
    1.30 @@ -181,7 +181,7 @@
    1.31  val SOME (t', asm) = common_nominator_p_ thy t;
    1.32  if term2str t' = 
    1.33    "(x + -1) * (-1 + x) / (1 * ((1 + x) * (-1 + x))) +\n(x + 1) * (1 + x) / (1 * ((1 + x) * (-1 + x)))"
    1.34 -  andalso terms2str asm = "[\"1 + x ~= 0\",\"-1 + x ~= 0\",\"1 ~= 0\"]"
    1.35 +  andalso terms2str asm = "[\"1 + x ~= 0\",\"-1 + x ~= 0\"]"
    1.36  then () else error "common_nominator_p_ 3 changed";
    1.37  
    1.38  "-------- fun add_fraction_p_ ------------------------------------------------";