1.1 --- a/test/Tools/isac/Knowledge/termorder.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/termorder.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -20,13 +20,13 @@
     1.4    val x4 = (term_of o the o (parse thy)) "x + a + b";
     1.5  
     1.6  if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
     1.7 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #1";
     1.8 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
     1.9   
    1.10  if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
    1.11 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #2";
    1.12 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
    1.13  
    1.14  if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
    1.15 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #3";
    1.16 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
    1.17  
    1.18    val aa = (term_of o the o (parse thy)) "-1 * a * x";
    1.19    val bb = (term_of o the o (parse thy)) "x^^^3";
    1.20 @@ -47,7 +47,7 @@
    1.21    val SOME (t',_) = 
    1.22        rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
    1.23  if term2str t' = "b + x + a" then ()
    1.24 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #11";
    1.25 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
    1.26  
    1.27    val NONE = 
    1.28        rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
    1.29 @@ -57,7 +57,7 @@
    1.30    val SOME (t',_) = 
    1.31        rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
    1.32  if term2str t' = "a + b + x" then ()
    1.33 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #13";
    1.34 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
    1.35  
    1.36  
    1.37  
    1.38 @@ -69,26 +69,26 @@
    1.39    term2str t';
    1.40    "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
    1.41  if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
    1.42 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #14";
    1.43 +else error "termorder.sml diff.behav ord_make_polynomial_in #14";
    1.44  
    1.45    val SOME (t',_) = 
    1.46        rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
    1.47  (*MG 2003...
    1.48    "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
    1.49  if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
    1.50 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #15";
    1.51 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
    1.52  
    1.53    val ttt' = "(3*x + 5)/18";
    1.54    val ttt = (term_of o the o (parse thy)) ttt';
    1.55    val SOME (uuu,_) = 
    1.56        rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
    1.57  if term2str uuu = "(5 + 3 * x) / 18" then ()
    1.58 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #16";
    1.59 +else error "termorder.sml diff.behav ord_make_polynomial_in #16";
    1.60  
    1.61    val SOME (uuu,_) = 
    1.62        rewrite_set_ thy false make_polynomial ttt;
    1.63  if term2str uuu = "(5 + 3 * x) / 18" then ()
    1.64 -else raise error "termorder.sml diff.behav ord_make_polynomial_in #16";
    1.65 +else error "termorder.sml diff.behav ord_make_polynomial_in #16";
    1.66  
    1.67  
    1.68