1.1 --- a/src/sml/IsacKnowledge/Rational.ML	Mon Sep 04 15:50:33 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Rational.ML	Mon Sep 04 15:53:35 2006 +0200
     1.3 @@ -598,7 +598,10 @@
     1.4  (*. datatypes for internal representation.*)
     1.5  type mv_monom = (int *      (*.coefficient or the monom.*)
     1.6  		 int list); (*.list of exponents)      .*)
     1.7 +fun mv_monom2str (i,is) = "("^int2str i^","^ints2str' is^")";
     1.8 +
     1.9  type mv_poly = mv_monom list; 
    1.10 +fun mv_poly2str p = (strs2str' o (map mv_monom2str)) p;
    1.11  
    1.12  (*. help function for monom_greater and geq .*)
    1.13  fun mv_mg_hlp([]) = EQUAL 

     2.1 --- a/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 15:50:33 2006 +0200
     2.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 15:53:35 2006 +0200
     2.3 @@ -2104,9 +2104,7 @@
     2.4     *)
     2.5  
     2.6  val mmm = (3,[2,1,1]);
     2.7 -fun mv_monom2str (i,is) = "("^int2str i^","^ints2str' is^")";
     2.8  mv_monom2str mmm;
     2.9  
    2.10  val xxx = [(1,[1,0,0]),(2,[1,1,0]),(3,[2,1,1])];
    2.11 -fun mv_poly2str p = (strs2str' o (map mv_monom2str)) p;
    2.12  mv_poly2str xxx;