1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4  (*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
     1.5  val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
     1.6  val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
     1.7 -if term2str t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
     1.8 +if UnparseC.term2str t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
     1.9  else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";
    1.10  "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
    1.11  (*WN.19.3.03 ---^-*)
    1.12 @@ -229,21 +229,21 @@
    1.13  (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
    1.14  val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
    1.15  val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
    1.16 -if term2str t' = "y ^^^ 2 + -2 * x * p = 0" then ()
    1.17 +if UnparseC.term2str t' = "y ^^^ 2 + -2 * x * p = 0" then ()
    1.18  else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
    1.19  
    1.20  (*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
    1.21  val t = str2term 
    1.22  "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
    1.23  val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
    1.24 -if term2str t' =
    1.25 +if UnparseC.term2str t' =
    1.26  "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) +\n-1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n-1 * y3 * (1 / 2) * x2 =\n0"
    1.27  then ()
    1.28  else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
    1.29  "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
    1.30  
    1.31  val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
    1.32 -if term2str t' = 
    1.33 +if UnparseC.term2str t' = 
    1.34  "A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + -1 * x1 * y2 / 2 + -1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n-1 * y3 * x2 / 2 =\n0"
    1.35  then ()
    1.36  else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
    1.37 @@ -286,19 +286,19 @@
    1.38  (* steps in rls d2_polyeq_bdv_only_simplify:*)
    1.39  
    1.40  (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
    1.41 -t |> term2str; t |> atomty;
    1.42 +t |> UnparseC.term2str; t |> atomty;
    1.43  val thm = num_str @{thm d2_prescind1};
    1.44 -thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
    1.45 -val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; term2str t';
    1.46 +thm |> Thm.prop_of |> UnparseC.term2str; thm |> Thm.prop_of |> atomty;
    1.47 +val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term2str t';
    1.48  
    1.49  (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1","")) 
    1.50                                                                          --> x = 0 | -6 + 5 * x = 0*)
    1.51 -t' |> term2str; t' |> atomty;
    1.52 +t' |> UnparseC.term2str; t' |> atomty;
    1.53  val thm = num_str @{thm d2_reduce_equation1};
    1.54 -thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
    1.55 -val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; term2str t'';
    1.56 +thm |> Thm.prop_of |> UnparseC.term2str; thm |> Thm.prop_of |> atomty;
    1.57 +val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term2str t'';
    1.58  (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
    1.59     instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
    1.60  *)
    1.61 -if term2str t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
    1.62 +if UnparseC.term2str t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
    1.63  else error "rls d2_polyeq_bdv_only_simplify broken";