1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml	Sun Jan 29 14:31:56 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Mon Jan 30 09:47:18 2023 +0100
     1.3 @@ -218,22 +218,22 @@
     1.4  val ctxt = @{context};
     1.5  (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
     1.6  (*WN.19.3.03 ---v-*)
     1.7 -(*3(b)*)val (bdv,v) = (TermC.parse_test @{context} "''bdv''", TermC.parse_test @{context} "R1");
     1.8 -val t = TermC.parse_test @{context} "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
     1.9 +(*3(b)*)val (bdv,v) = (ParseC.parse_test @{context} "''bdv''", ParseC.parse_test @{context} "R1");
    1.10 +val t = ParseC.parse_test @{context} "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
    1.11  val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
    1.12  if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
    1.13  else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
    1.14  "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
    1.15  (*WN.19.3.03 ---^-*)
    1.16  
    1.17 -(*3(c)*)val (bdv,v) = (TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "p");
    1.18 -val t = TermC.parse_test @{context} "y \<up> 2 + - 2 * (x * p) = 0";
    1.19 +(*3(c)*)val (bdv,v) = (ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "p");
    1.20 +val t = ParseC.parse_test @{context} "y \<up> 2 + - 2 * (x * p) = 0";
    1.21  val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
    1.22  if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
    1.23  else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
    1.24  
    1.25 -(*3(d)*)val (bdv,v) = (TermC.parse_test @{context} "''bdv''", TermC.parse_test @{context} "x2");
    1.26 -val t = TermC.parse_test @{context} 
    1.27 +(*3(d)*)val (bdv,v) = (ParseC.parse_test @{context} "''bdv''", ParseC.parse_test @{context} "x2");
    1.28 +val t = ParseC.parse_test @{context} 
    1.29  "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.30  val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
    1.31  if UnparseC.term t' =
    1.32 @@ -249,13 +249,13 @@
    1.33  else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
    1.34  "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) + - 1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - 1 * y3 * (1 / 2)) * x2 = 0";
    1.35  
    1.36 -(*3(e)*)val (bdv,v) = (TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "a");
    1.37 -val t = TermC.parse_test @{context} 
    1.38 +(*3(e)*)val (bdv,v) = (ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "a");
    1.39 +val t = ParseC.parse_test @{context} 
    1.40  "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
    1.41  val NONE = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
    1.42  (* the invisible parentheses are as expected *)
    1.43  
    1.44 -val t = TermC.parse_test @{context} "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
    1.45 +val t = ParseC.parse_test @{context} "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
    1.46  rewrite_set_ ctxt false expand_binoms t;
    1.47  
    1.48  
    1.49 @@ -278,8 +278,8 @@
    1.50  "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
    1.51  "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
    1.52  "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
    1.53 -val t = TermC.parse_test @{context} "-6 * x + 5 * x \<up> 2 = (0::real)";
    1.54 -val subst = [(TermC.parse_test @{context} "(bdv::real)", TermC.parse_test @{context} "(x::real)")];
    1.55 +val t = ParseC.parse_test @{context} "-6 * x + 5 * x \<up> 2 = (0::real)";
    1.56 +val subst = [(ParseC.parse_test @{context} "(bdv::real)", ParseC.parse_test @{context} "(x::real)")];
    1.57  val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t;
    1.58  (* steps in rls d2_polyeq_bdv_only_simplify:*)
    1.59