wneuper/isa: comparison test/Tools/isac/Knowledge/rational.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 print("\n\n*********************   rational.sml - TESTS    *************************\n\n");
 print("\n\n***** divide tests *****\n");
 val mv_pquot1 = (#1(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
 (* result: [(1,[0,0,1]),(1,[0,0,0])] *)
-if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
+if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else error ("rational.sml: example failed");
 val mv_prest1 = (#2(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
 (* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
-if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else raise error ("rational.sml: example failed");
+if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else error ("rational.sml: example failed");
 val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
 (* result: [(4,[1]),(4,[0])] *)
-if mv_pquot2=[(4,[1]),(4,[0])] then () else raise error ("rational.sml: example failed");
+if mv_pquot2=[(4,[1]),(4,[0])] then () else error ("rational.sml: example failed");
 val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
 (* result: [(12,[0]] *)
-if mv_prest2=[(12,[0])] then () else raise error ("rational.sml: example failed");
+if mv_prest2=[(12,[0])] then () else error ("rational.sml: example failed");
 val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
 (* [(2,[1]),(~2,[0])] *)
-if mv_pquot3=[(2,[1]),(~2,[0])] then () else raise error ("rational.sml: example failed");
+if mv_pquot3=[(2,[1]),(~2,[0])] then () else error ("rational.sml: example failed");
 val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
 (* [(1,[2]),(~1,[0])] *)
-if mv_prest3=[(1,[2]),(~1,[0])] then () else raise error ("rational.sml: example failed");
+if mv_prest3=[(1,[2]),(~1,[0])] then () else error ("rational.sml: example failed");
 val mv_pquot4 = (#1(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1])],[(2,[1,0,0]),(4,[0,0,1])],LEX_)));
 (* [(1,[0,1,1])] *)
-if mv_pquot4=[(1,[0,1,1])] then () else raise error ("rational.sml: example failed");
+if mv_pquot4=[(1,[0,1,1])] then () else error ("rational.sml: example failed");
 val mv_prest4 = (#2(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1])],[(2,[1,0,0]),(4,[0,0,1])],GGO_)));
 (* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
-if mv_prest4 =[(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
+if mv_prest4 =[(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
 val mv_pquot5 = (#1(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1]),(6,[2,1,3]),(4,[0,4,1]),(1,[2,2,1])],[(1,[0,0,1])],LEX_)));
 (* [(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])]*)
-if mv_pquot5=[(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])] then () else raise error ("rational.sml: example failed");
+if mv_pquot5=[(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])] then () else error ("rational.sml: example failed");
 val mv_prest5 = (#2(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1]),(6,[2,1,3]),(4,[0,4,1]),(1,[2,2,1])],[(1,[0,0,1])],LEX_)));
 (* [] *)
-if mv_prest5=[] then () else raise error ("rational.sml: example failed");
+if mv_prest5=[] then () else error ("rational.sml: example failed");
 (* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
 val mv_pquot6 = (#1(mv_division([(1,[2,0,0]),(2,[1,1,0]),(2,[1,0,0]),(1,[0,2,0]),(2,[0,1,0]),(1,[0,0,0])],[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])],LEX_)));
-if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
+if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else error ("rational.sml: example failed");
 val mv_prest6 = (#2(mv_division([(1,[2,0,0]),(2,[1,1,0]),(2,[1,0,0]),(1,[0,2,0]),(2,[0,1,0]),(1,[0,0,0])],[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])],LEX_)));
-if mv_prest6=[] then () else raise error ("rational.sml: example failed");
+if mv_prest6=[] then () else error ("rational.sml: example failed");
 print("\n\n***** MV_CONTENT-TESTS *****\n");
 val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
 (* [(1,[0,1]),(1,[0,0])] *)
-if  mv_cont1=[(1,[0,1]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
+if  mv_cont1=[(1,[0,1]),(1,[0,0])] then () else error ("rational.sml: example failed");
 val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
 (*[(1,[1,0]),(1,[0,0])]*)
-if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
+if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else error ("rational.sml: example failed");
 val mv_cont2=mv_content([(2,[1]),(4,[0])]);
 (* [(2,[0])] *)
-if mv_cont2=[(2,[0])] then () else raise error ("rational.sml: example failed");
+if mv_cont2=[(2,[0])] then () else error ("rational.sml: example failed");
 val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
 (* [(1,[1]),(2,[0])] *)
-if mv_pp2=[(1,[1]),(2,[0])] then () else raise error ("rational.sml: example failed");
+if mv_pp2=[(1,[1]),(2,[0])] then () else error ("rational.sml: example failed");
 val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
 (* [(2,[0,0,0])] *)
-if mv_cont3=[(2,[0,0,0])] then () else raise error ("rational.sml: example failed");
+if mv_cont3=[(2,[0,0,0])] then () else error ("rational.sml: example failed");
 val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
 (* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
-if mv_pp3=[(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] then () else raise error ("rational.sml: example failed");
+if mv_pp3=[(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] then () else error ("rational.sml: example failed");
 val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
 (* [(1,[0,0,0])] *)
-if mv_cont4=[(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
+if mv_cont4=[(1,[0,0,0])] then () else error ("rational.sml: example failed");
 val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
 (* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
-if mv_pp4=[(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
+if mv_pp4=[(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
 val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
 (* [(3,[0,0])] *)
-if con1=[(3,[0,0])] then () else raise error ("rational.sml: example failed");
+if con1=[(3,[0,0])] then () else error ("rational.sml: example failed");
 val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
 (* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
-if pp1=[(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] then () else raise error ("rational.sml: example failed");
+if pp1=[(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] then () else error ("rational.sml: example failed");
 val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
 (* [(1,[0,0])] *)
-if con2=[(1,[0,0])] then () else raise error ("rational.sml: example failed");
+if con2=[(1,[0,0])] then () else error ("rational.sml: example failed");
 val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
 (* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
-if pp2=[(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] then () else raise error ("rational.sml: example failed");
+if pp2=[(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] then () else error ("rational.sml: example failed");
 val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
 (* [(3,[0,1,0])] *)
-if cont1=[(3,[0,1,0])] then () else raise error ("rational.sml: example failed");
+if cont1=[(3,[0,1,0])] then () else error ("rational.sml: example failed");
 val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
 (* [(1,[2,0,0])] *)
-if pp1=[(1,[2,0,0])] then () else raise error ("rational.sml: example failed");
+if pp1=[(1,[2,0,0])] then () else error ("rational.sml: example failed");
 val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
 (* [(2,[0,1,0])] *)
-if cont2=[(2,[0,1,0])] then () else raise error ("rational.sml: example failed");
+if cont2=[(2,[0,1,0])] then () else error ("rational.sml: example failed");
 val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
 (* [(1,[2,0,0]),(2,[1,1,0])] *)
-if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else raise error ("rational.sml: example failed");
+if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else error ("rational.sml: example failed");
 print("\n\n\n\n********************************************************\n\n");
 val cont3=mv_content [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
-if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
+if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else error ("rational.sml: example failed");
 val pp3=mv_pp [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
 "-------- fun monom2term,  fun poly2term' ------------------------";
 "-------- fun monom2term,  fun poly2term' ------------------------";
 fun parse_rat str = (term_of o the o (parse thy)) str;
 print("\n\n***** mv_gcd-tests *****\n");
 val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
 (* [(2,[1,1]),(2,[0,0])] *)
-if ggt1=[(2,[1,1]),(2,[0,0])] then () else raise error ("rational.sml: example failed");
+if ggt1=[(2,[1,1]),(2,[0,0])] then () else error ("rational.sml: example failed");
 val ggt2 = mv_gcd [(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(15,[1,1,1])] [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
 (* [(2,[1,1,0]),(3,[0,0,1])] *)
-if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
+if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
 val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
 (* [(1,[1,0]),(~1,[0,1])] *)
-if ggt3=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
+if ggt3=[(1,[1,0]),(~1,[0,1])] then () else error ("rational.sml: example failed");
 val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
 (* [(1,[1,0,0])] *)
-if ggt4=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
+if ggt4=[(1,[1,0,0])] then () else error ("rational.sml: example failed");
 val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
 (* [(1,[1,0]),(~1,[0,1])] *)
-if ggt5=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
+if ggt5=[(1,[1,0]),(~1,[0,1])] then () else error ("rational.sml: example failed");
 val ggt6 = mv_gcd [(10,[2,1,1]),(14,[1,1,0]),(3,[1,0,1]),(20,[1,2,1])] [(5,[1,1,1]),(7,[2,1,1])];
 (* [(1,[0,0,0])] *)
-if ggt6=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
+if ggt6=[(1,[1,0,0])] then () else error ("rational.sml: example failed");
 print("\n\n***** kgv-tests *****\n");
 val kgv1=mv_lcm [(10,[])] [(15,[])];
 (* [(30,[])] *)
-if kgv1=[(30,[])] then () else raise error ("rational.sml: example failed");
+if kgv1=[(30,[])] then () else error ("rational.sml: example failed");
 val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
 (* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
-if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else raise error ("rational.sml: example failed");
+if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else error ("rational.sml: example failed");
 val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
 (* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
-if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else raise error ("rational.sml: example failed");
+if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else error ("rational.sml: example failed");
 (*!!!--------
 print("\n\n***** STEP_CANCEL_TESTS: *****\n");
 val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) /  (6 * a * c)";
 val div2 = term2str (step_cancel term2);
-if div2 =  "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else raise error ("rational.sml: example failed");
+if div2 =  "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else error ("rational.sml: example failed");
 val term1 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) / a";
 val div1  = term2str(step_cancel term1);
-if div1 =  "(3 * c + 14 * b + 20 * (b ^^^ 2 * c) + 10 * (a * (b * c))) * a / (1 * a)" then () else raise error ("rational.sml: example failed");
+if div1 =  "(3 * c + 14 * b + 20 * (b ^^^ 2 * c) + 10 * (a * (b * c))) * a / (1 * a)" then () else error ("rational.sml: example failed");
 val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
 val div3 = term2str(step_cancel term3);
-if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else  raise error ("rational.sml: example failed");
+if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else  error ("rational.sml: example failed");
 --------------------------------------------------------------------------!!!*)
 (*-----versuche 13.3.03-----
 val t = str2term "1 - x^^^2 - 5 * x^^^5";
 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
 val SOME (t',_) = common_nominator_ thy t;
 val SOME (t'',_) = add_fraction_ thy t;
 if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\
 \ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then ()
-else raise error "rational.sml lex-ord 1";
+else error "rational.sml lex-ord 1";
 if term2str t'' = "(-1 - y - x) / (y - x)" then ()
-else raise error "rational.sml lex-ord 2";
+else error "rational.sml lex-ord 2";
 (*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*)
 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
 val SOME (t',_) = norm_expanded_rat_ thy t;
 if term2str t' = "(x + y) / (x - y)" then ()
-else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
+else error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
 (*val SOME (t'',_) = norm_rational_ thy t;
 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
 WN.16.10.02 ?! + WN060831???SK4
 WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*)
 val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
 val SOME (t',_) = norm_expanded_rat_ thy t;
 if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then ()
-else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
+else error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
 (*val SOME (t'',_) = norm_rational_ thy t;
 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!
 WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*)
 val t=(term_of o the o (parse thy))
 val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*)
 val e188a = the (rewrite_set thy' false "cancel" e188a');
 is_expanded (parse_rat "8 * x + -8");
 (* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
 if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
-else raise error "rational.sml: e188a new behaviour";
+else error "rational.sml: e188a new behaviour";
 val SOME (t,_) = rewrite_set thy' false mp
 			     "(8*((-1) + x))/(9*((-1) + x))";
 print("b)\n");
 val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
 val SOME (t,_) = rewrite_set thy' false "cancel" e188b';
 val e188c = the (rewrite_set thy' false "cancel_p" e188c');
 (*is_expanded (parse_rat "a + -1 * b");*)
 val SOME (t,_) =
 rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
 if t= "(a + -1 * b) / (-1 * a + b)"  then()
-else raise error "rational.sml: e188c new behaviour";
+else error "rational.sml: e188c new behaviour";
 print("\n\nexample 190:\n");
 print("c)\n");
 val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
 val e190c = the (rewrite_set thy' false "cancel" e190c');
 val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
 if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
-else raise error "rational.sml: e190c new behaviour";
+else error "rational.sml: e190c new behaviour";
 print("\n\nexample 191:\n");
 print("a)\n");
 val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )";
 (*WN.23.10.02-------
 is_expanded (parse_rat "x + y");
 true; -----------*)
 val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
 (* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
 if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
-else raise error "rational.sml: e191a new behaviour";
+else error "rational.sml: e191a new behaviour";
 print("c)\n");
 val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
 (*WN.23.10.02-------
 val e191c = the (rewrite_set thy' false "cancel" e191c');
 is_expanded (parse_rat "-25 + 9*x^^^2");
 true;------------*)
 val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
 (* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
 if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
-else raise error "rational.sml: 'e191c' new behaviour";
+else error "rational.sml: 'e191c' new behaviour";
 print("\n\nexample 192:\n");
 print("b)\n");
 val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 *  y^^^3 )";
 val e192b = the (rewrite_set thy' false "cancel" e192b');
 -------------------*)
 val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
 if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)"
 (*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*)
-then () else raise error "rational.sml: 'e192b' new behaviour";
+then () else error "rational.sml: 'e192b' new behaviour";
 (*^^^ works with MG's simplifier vvv*)
 val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
 val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
-if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else raise error "rational.sml: 'e192b'MG new behaviour";
+if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else error "rational.sml: 'e192b'MG new behaviour";
 print("\n\nexample 193:\n");
 print("a)\n");
 val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
 val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
 val SOME (t,_) = rewrite_set thy' false "cancel" wn01;
 (* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
 if t = "(-5 + 3 * x) / 1" then ()
-else raise error "rational.sml: new behav. in cancel wn01";
+else error "rational.sml: new behav. in cancel wn01";
 "-------- common_nominator_p ---------------------------- --------";
 "-------- common_nominator_p ---------------------------- --------";
 "-------- common_nominator_p ---------------------------- --------";
 val rls' = "common_nominator_p";
 print("\n\nexample stiefel:\n");
 val est1'="(7) / (-14) + (-2) / (4)";
 val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
 if est1 = ("-1 / 1",[]) then ()
-else raise error "new behaviour in rational.sml: est1'";
+else error "new behaviour in rational.sml: est1'";
 val t = (term_of o the o (parse thy))
 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
 val SOME (t',_) = factout_ thy t;
 term2str t';
 val SOME r = nex revsets t;
 val (r,(t,asm))::_ = loc revsets t r;
 val ss = term2str t;
 if ss = "(3 - x) / (3 + x)" then ()
-else raise error "rational.sml: new behav. in rev-set cancel";
+else error "rational.sml: new behav. in rev-set cancel";
 terms2str asm;
 "-------- 'reverse-ruleset' cancel_p -----------------------------";
 "-------- 'reverse-ruleset' cancel_p -----------------------------";
 "-------- norm_Rational ------------------------------------------";
 "-------- norm_Rational ------------------------------------------";
 "-------- norm_Rational ------------------------------------------";
 val t = str2term "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1";
+if term2str t' = "1 / 18 = 0" then () else error "rational.sml 1";
 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
-else raise error "rational.sml 2";
+else error "rational.sml 2";
 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
-else raise error "rational.sml 3";
+else error "rational.sml 3";
 (*trace_rewrite:=true;*)
 val t = str2term "Not (6*x is_atom)";
 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
 "True";
 val t = str2term "1 < 2";
 term2str t';
 trace_rewrite:=false;
 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4";
+if term2str t' = "65 * x / 2" then () else error "rational.sml 4";
 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
-else raise error "rational.sml 5";
+else error "rational.sml 5";
 (*SRAM Schalk I, p.92 Nr. 609a*)
 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 if term2str t' = "(-255 + 112 * x) / 135" then ()
-else raise error "rational.sml 6";
+else error "rational.sml 6";
 (*SRAM Schalk I, p.92 Nr. 610c*)
 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7";
+if term2str t' = "(-3 + -1 * x) / 2" then () else error "rational.sml 7";
 (*SRAM Schalk I, p.92 Nr. 476a*)
 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\
 		 \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-(*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*)
+(*if term2str t' = "1 / 1" then () else error "rational.sml 8";3.6.03*)
-if term2str t' = "1" then () else raise error "rational.sml 8";
+if term2str t' = "1" then () else error "rational.sml 8";
 (*............................vvv---TODO: sollte gehen mit poly_order *)
 (*Schalk I, p.92 Nr. 472a*)
 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a";
+if term2str t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
 		 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
 		 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
 (*SRA Schalk I, p.40 Nr. 164b *)
 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) = "19 / 21" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
 (*SRA Schalk I, p.40 Nr. 166a *)
 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) = "45 / 2" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
 "-------- cancellation -------------------------------------------";
 "-------- cancellation -------------------------------------------";
 "-------- cancellation -------------------------------------------";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
 (* e192b Stefan K.*)
 val t = str2term
 "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "x ^^^ 2 / y ^^^ 2"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
 (*SRC Schalk I, p.66 Nr. 379c *)
 val t = str2term
 "(a - b)/(b - a)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "-1"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
 (*SRC Schalk I, p.66 Nr. 380b *)
 val t = str2term
 "15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(27 + 12 * x) / (28 + 8 * x)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
 (*Schalk I, p.60 Nr. 215c *)
 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
 (* WN060831????MG1
 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
 *)
 (*val t = str2term
 "(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
 term2str t;*)
 val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(a + b) / (4 * a + -4 * b)"
-then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
+then () else error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
 *)
 (*SRC Schalk I, p.66 Nr. 381b *)
 val t = str2term
 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "-1 / (5 + -2 * x)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
 (*SRC Schalk I, p.66 Nr. 381c *)
 val t = str2term
 "(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
 (*SRC Schalk I, p.66 Nr. 383a *)
 val t = str2term
 "(5*a^^^2 - 5*a*b)/(a - b)^^^2";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "5 * a / (a + -1 * b)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
 "-------- common denominator -------------------------------------";
 "-------- common denominator -------------------------------------";
 "-------- common denominator -------------------------------------";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
 (*SRA Schalk I, p.67 Nr. 407b *)
 val t = str2term
 "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "4 / c"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
 (*SRA Schalk I, p.67 Nr. 410b *)
 val t = str2term
 "1/(x+1) + 1/(x+2) - 2/(x+3)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
 (*SRA Schalk I, p.67 Nr. 413b *)
 val t = str2term
 "(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "6 * x / (1 + -1 * x ^^^ 2)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
 (*SRA Schalk I, p.68 Nr. 414a *)
 val t = str2term
 "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
 (*SRA Schalk I, p.68 Nr. 423a *)
 val t = str2term
 "(2*x+3*y)/x + (4*x^^^3 - x*y^^^2 - 3*y^^^3)/(x^^^3 - 2*x^^^2*y+x*y^^^2) - (5*x+6*y)/(x - y)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "1"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
 (*SRA Schalk I, p.68 Nr. 428b *)
 val t = str2term
 "1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
 (*SRA Schalk I, p.68 Nr. 430b *)
 val t = str2term
 "a^^^2/(a - 3*b) - 108*a*b^^^3/((a+3*b)*(a^^^2 - 9*b^^^2)) - 9*b^^^2*(a - 3*b)/(a+3*b)^^^2";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "a + 3 * b"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
 (*SRA Schalk I, p.68 Nr. 432 *)
 val t = str2term
 "(a^^^2+a*b)/(a^^^2 - b^^^2) - (b^^^2 - a*b)/(b^^^2 - a^^^2) + a^^^2*(a - b)/(a^^^3 - a^^^2*b) - 2*a*(a^^^2 - b^^^2)/(a^^^3 - a*b^^^2) - 2*b^^^2/(a^^^2 - b^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "0"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
 (*Eigenes*)
 val t = str2term
 "3*a/(a*b) + x/y";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(3 * y + b * x) / (b * y)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
 "-------- multiply and cancel ------------------------------------";
 "-------- multiply and cancel ------------------------------------";
 "-------- multiply and cancel ------------------------------------";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(5 * x + -5 * y) / (18 * x + 18 * y)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
 (*SRM.test Schalk I, p.68 Nr. 436b *)
 (*WN060420???MG3 crashes with method 'simplify' in
 IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "5 * a / (a + -1 * b)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
 (*Schalk I, p.68 Nr. 437a *)
 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 if (term2str t) = "1 / (4 * c + 3 * e)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
 "----- S.K. corrected non-termination 060904";
 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
 if term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)" then ()
-else raise error "rational.sml.sml: S.K.8..corrected 060904-6";
+else error "rational.sml.sml: S.K.8..corrected 060904-6";
 "----- S.K. corrected non-termination of cancel_p_";
 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
 if term2str t' = "1 / (4 * c + 3 * e)" then ()
-else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
+else error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
 (**)
 (*Schalk I, p.68 Nr. 437b *)
 (* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "x ^^^ 2"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
 (*SRM Schalk I, p.68 Nr. 439b *)
 val t = str2term
 "(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(x + -4 * x ^^^ 3) / 2"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
 (*SRM Schalk I, p.68 Nr. 440a *)
 val t = str2term
 "(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-3 + x) / (2 + x)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
 val t = str2term
 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational 27";
+else error "rational.sml.sml: diff.behav. in norm_Rational 27";
 "----- SK12 works since 0707xx";
 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational 28";
+else error "rational.sml.sml: diff.behav. in norm_Rational 28";
 "-------- common denominator and multiplication ------------------";
 "-------- common denominator and multiplication ------------------";
 "-------- common denominator and multiplication ------------------";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
 (*SRAM Schalk I, p.69 Nr. 442b *)
 val t = str2term "(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x)*(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
 (*SRAM Schalk I, p.69 Nr. 443b *)
 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
 (*SRAM Schalk I, p.69 Nr. 445b *)
 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "a ^^^ 3 / 27"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
 (*SRAM Schalk I, p.69 Nr. 446b *)
 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
 val t = str2term
 "(2*x^^^2/(3*y)+x/y^^^2)*(4*x^^^4/(9*y^^^2)+x^^^2/y^^^4)*(2*x^^^2/(3*y) - x/y^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
 (*SRAM Schalk I, p.69 Nr. 450a *)
 val t = str2term
 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
 "-------- double fractions ---------------------------------------";
 "-------- double fractions ---------------------------------------";
 "-------- double fractions ---------------------------------------";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
 (*SRD Schalk I, p.69 Nr. 455a *)
 val t = str2term
 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
 "----- Schalk I, p.69 Nr. 455b";
 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
 "----- ?: worked before 0707xx";
 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "-1 / (3 + y)" then ()
-else raise error "rational.sml: -1 / (3 + y) norm_Rational";
+else error "rational.sml: -1 / (3 + y) norm_Rational";
 (*SRD Schalk I, p.69 Nr. 456b *)
 val t = str2term
 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
 (*SRD Schalk I, p.69 Nr. 457b *)
 val t = str2term
 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
 "----- Schalk I, p.69 Nr. 458b works since 0707";
 val t = str2term
 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
 (*SRD Schalk I, p.69 Nr. 459b *)
 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
 (*Schalk I, p.69 Nr. 460b nonterm.SK
 val t = str2term
 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 if term2str t =
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
 val t = str2term
 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
 ... non terminating.
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "x + y"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
 (*----------------------------------------------------------------------*)
 (*---------------------- Einfache Dppelbrche --------------------------*)
 (*----------------------------------------------------------------------*)
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "1 / 2"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
 (*SRD Schalk I, p.69 Nr. 464b *)
 val t = str2term
 "(a - a/(a - 2)) / (a + a/(a - 2))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(3 + -1 * a) / (1 + -1 * a)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
 (*SRD Schalk I, p.69 Nr. 465b *)
 val t = str2term
 "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(4 * x + 6 * y + -9 * z) / (4 * x)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
 (*SRD Schalk I, p.69 Nr. 466b *)
 val t = str2term
 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(25 + -10 * x + x ^^^ 2) / 18"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
 (*SRD Schalk I, p.70 Nr. 469 *)
 val t = str2term
 "3*b^^^2/(4*a^^^2 - 8*a*b + 4*b^^^2)/(a/(a^^^2*b - b^^^3) + (a - b)/(4*a*b^^^2+4*b^^^3) - 1/(4*b^^^2))";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "3 * b ^^^ 3 / (2 * a + -2 * b)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
 (*----------------------------------------------------------------------*)
 (*---------------------- Mehrfache Dppelbrueche ------------------------*)
 (*----------------------------------------------------------------------*)
 (*WN060419 crashes with method 'simplify' ????SK*)
 val t = str2term
 "((a^^^2 - b^^^2)/(2*a*b)+2*a*b/(a^^^2 - b^^^2))/((a^^^2+b^^^2)/(2*a*b)+1) / ((a^^^2+b^^^2)^^^2/(a+b)^^^2)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
 "----- Schalk I, p.70 Nr. 477a";
 (* MG Achtung: terme explodieren; Bsp zu komplex;
 L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
 val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
 		 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 if term2str t' =
 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
 (* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
 if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /\n(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) *\n (a + -1 * b))" then ()
-else raise error "rational.sml: works again";
+else error "rational.sml: works again";
 re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
 (*Schalk I, p.70 Nr. 480a *)
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
 (*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
 val t = str2term
 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 (*--------------------------------------------------------------------*)
 "---- MGs test set";
 val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
 val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
 if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
-else raise error "";
+else error "";
 (*--------------------------------------------------------------------*)
 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
 ---> Sortierung FALSCH !!  *)
 val t = str2term "b^^^3 * a^^^5/a ";
 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
 "----- MGs test set";
 val t = str2term "(a^^^2 + -1)/(a+1)";
 val SOME (t',_) = rewrite_set_ thy false cancel_p t;
 if term2str t' = "(-1 + a) / 1" then ()
-else raise error "rational.sml MG tests 3d";
+else error "rational.sml MG tests 3d";
 "----- NOT TERMINATING ?: worked before 0707xx";
 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
 val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
 if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
-else raise error "rational.sml MG tests 3e";
+else error "rational.sml MG tests 3e";
 "----- corrected SK060905";
 val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 if term2str t' = "-1 / (5 + -2 * x)" then ()
-else raise error "rational.sml corrected SK060905";
+else error "rational.sml corrected SK060905";
 "--------------------------------------------------------------------";
 "----------------------- Muster-Beispiele fuer DA -------------------";
 "--------------------------------------------------------------------";
 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
 then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
+else error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
 "-------- me Schalk I No.186 -------------------------------------";
 "-------- me Schalk I No.186 -------------------------------------";
 "-------- me Schalk I No.186 -------------------------------------";
 val fmz = ["TERM ((14 * x * y) / ( x * y ))",
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
 case (f2str f, nxt) of
 ("14", ("End_Proof'", _)) => ()
-| _ => raise error "rational.sml diff.behav. in me Schalk I No.186";
+| _ => error "rational.sml diff.behav. in me Schalk I No.186";
 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
 interSteps 1 ([2,1],Res);
 val ((pt,p),_) = get_calc 1; show_pt pt;
 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
 (*if length newnds = 12 then () WN060905*)
 if length newnds = 13 then ()
-else raise error "rational.sml: interSteps cancel_p rev_rew_p";
+else error "rational.sml: interSteps cancel_p rev_rew_p";
 val p = ([2,1,9],Res);
 getTactic 1 p;
 val (_, tac, _) = pt_extract (pt, p);
 (*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
 WN060905*)
 case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
-| _ => raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
+| _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
 "-------- investigate rulesets for cancel_p ----------------------";
 "-------- investigate rulesets for cancel_p ----------------------";
 "-------- investigate rulesets for cancel_p ----------------------";
 "----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
 if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
-else raise error "rational.sml SK060904-1a worked since 0707xx";
+else error "rational.sml SK060904-1a worked since 0707xx";
 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
 val SOME (t',_) = cancel_p_ thy t;
 if term2str t' = "1 / (4 * c + 3 * e)" then ()
-else raise error "rational.sml SK060904-1b";
+else error "rational.sml SK060904-1b";
 "----- SK060904-2a non-termination of add_fraction_p_";
 val t = str2term " (a + b * x) / (a + -1 * (b * x)) +  \
 		 \ (-1 * a + b * x) / (a + b * x)      ";
 "-------- how to stepwise construct Scripts ----------------------";
 "-------- how to stepwise construct Scripts ----------------------";
 "-------- how to stepwise construct Scripts ----------------------";
-lse raise error "rational.sml SK060904-1a worked since 0707xx";
+lse error "rational.sml SK060904-1a worked since 0707xx";
 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
 val SOME (t',_) = cancel_p_ thy t;
 if term2str t' = "1 / (4 * c + 3 * e)" then ()
-else raise error "rational.sml SK060904-1b";
+else error "rational.sml SK060904-1b";
 "----- SK060904-2a non-termination of add_fraction_p_";
 val t = str2term " (a + b * x) / (a + -1 * (b * x)) +  \
 		 \ (-1 * a + b * x) / (a + b * x)      ";
 "-------- how to stepwise construct Scripts ----------------------";
 "-------- how to stepwise construct Scripts ----------------------";
 "-------- how to stepwise construct Scripts ----------------------";
-lse raise error "rational.sml SK060904-1a worked since 0707xx";
+lse error "rational.sml SK060904-1a worked since 0707xx";
 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
 val SOME (t',_) = cancel_p_ thy t;
 if term2str t' = "1 / (4 * c + 3 * e)" then ()
-else raise error "rational.sml SK060904-1b";
+else error "rational.sml SK060904-1b";
 "----- SK060904-2a non-termination of add_fraction_p_";
 val t = str2term " (a + b * x) / (a + -1 * (b * x)) +  \
 		 \ (-1 * a + b * x) / (a + b * x)      ";

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37991	028442673981
child 38034	928cebc9c4aa