1.1 --- a/test/Tools/isac/Knowledge/rlang.sml	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -210,12 +210,12 @@
     1.4  val t = (Thm.term_of o the o (parse thy)) "3 * x / 5";
     1.5  val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true 
     1.6  				    [ (bdv, v) ] make_ratpoly_in t;
     1.7 -if term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1";
     1.8 +if UnparseC.term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1";
     1.9  
    1.10  val t = str2term "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";
    1.11  val subst = [(str2term "bdv", str2term "x")];
    1.12  val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
    1.13 -if term2str t' = "1 / 18 = 0" then () else error "rlang.sml: 2";
    1.14 +if UnparseC.term2str t' = "1 / 18 = 0" then () else error "rlang.sml: 2";
    1.15  (*WN---^ *)
    1.16  
    1.17  (*-----------------  Schalk I s.87 Bsp 36b ------------------------*)
    1.18 @@ -252,8 +252,8 @@
    1.19  val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
    1.20  val subst = [(str2term "bdv", str2term "x")];
    1.21  val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
    1.22 -term2str t';
    1.23 -if term2str t' = "79 / 12 + 65 / 36 * x = 0" then () 
    1.24 +UnparseC.term2str t';
    1.25 +if UnparseC.term2str t' = "79 / 12 + 65 / 36 * x = 0" then () 
    1.26  else error "rlang.sml: 3";
    1.27  (*WN---^ *)
    1.28  
    1.29 @@ -376,13 +376,13 @@
    1.30  val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
    1.31  val subst = [(str2term "bdv", str2term "x")];
    1.32  val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
    1.33 -if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then () 
    1.34 +if UnparseC.term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then () 
    1.35  else error "rlang.sml: 4";
    1.36  
    1.37  val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 + (6*x)^^^2 - 29";
    1.38  val subst = [(str2term "bdv", str2term "x")];
    1.39  val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
    1.40 -if term2str t' = "-35 + 35 * x" then () 
    1.41 +if UnparseC.term2str t' = "-35 + 35 * x" then () 
    1.42  else error "rlang.sml: 4.1";
    1.43  (*WN---^ *)
    1.44  
    1.45 @@ -730,8 +730,8 @@
    1.46  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
    1.47  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
    1.48  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
    1.49 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (Ctree.get_assumptions pt p);
    1.50 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (Ctree.get_assumptions pt p);
    1.51 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;UnparseC.terms2str (*WN1104changed*) (Ctree.get_assumptions pt p);
    1.52 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;UnparseC.terms2str (*WN1104changed*) (Ctree.get_assumptions pt p);
    1.53  
    1.54  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
    1.55  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
    1.56 @@ -887,7 +887,7 @@
    1.57  then writeln "only [x = 4] !\nonly [x = 4] !\nonly [x = 4] !\n"
    1.58  else error "rlang.sml: diff.behav. in II 68a";
    1.59  val asms = Ctree.get_assumptions pt p;
    1.60 -if terms2str (*WN1104changed*) asms = 
    1.61 +if UnparseC.terms2str (*WN1104changed*) asms = 
    1.62  "[0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56,\
    1.63   \0 <= 1 / 9,\
    1.64   \0 <= 1 / 9,\
    1.65 @@ -1421,7 +1421,7 @@
    1.66  val t = str2term"(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)";
    1.67  trace_rewrite := false;
    1.68  val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
    1.69 -term2str t';
    1.70 +UnparseC.term2str t';
    1.71  trace_rewrite:=false;
    1.72  
    1.73  #  rls: norm_Rational on: (a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) = 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)
    1.74 @@ -1615,7 +1615,7 @@
    1.75  val t = str2term "(2*x+1)*x^^^2 = 0";
    1.76  val subst = [(str2term "bdv", str2term "x")];
    1.77  val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
    1.78 -if term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then () 
    1.79 +if UnparseC.term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then () 
    1.80  else error "rlang.sml: 7";
    1.81  *)
    1.82  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.83 @@ -1640,7 +1640,7 @@
    1.84    "(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x";
    1.85  > val SOME (t',asm) = 
    1.86        rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t;
    1.87 -> term2str t'; terms2str asm;
    1.88 +> UnparseC.term2str t'; UnparseC.terms2str asm;
    1.89  "(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3)"
    1.90  "[\"9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0\",\"x ~= 0\"]"
    1.91  > trace_rewrite:=false;
    1.92 @@ -1686,7 +1686,7 @@
    1.93  val asms = Ctree.get_assumptions pt p;
    1.94  (*if asms = [str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)",
    1.95               str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)"]*)
    1.96 -if terms2str (*WN1104changed*) asms = 
    1.97 +if UnparseC.terms2str (*WN1104changed*) asms = 
    1.98     "[0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1),\
    1.99     \0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1)]"
   1.100  then writeln"simplify result\nsimplify result\nsimplify result"