1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  val thy = @{theory Complex_Main};
     1.5  val ctxt = @{context};
     1.6  val thm = @{thm add.commute};
     1.7 -val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
     1.8 +val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)";
     1.9  "----- from old: fun rewrite__";
    1.10  val bdv = [];
    1.11  val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
    1.12 @@ -488,7 +488,7 @@
    1.13  "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
    1.14  val thy = @{theory RatEq};
    1.15  val ctxt = Proof_Context.init_global thy;
    1.16 -val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
    1.17 +val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
    1.18  val rls = assoc_rls "RatEq_eliminate"
    1.19  
    1.20  val SOME (t''''', asm''''') =