diff -r ba258eeb0826 -r 2197e3597cba test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy
--- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Mon Jan 30 12:38:17 2023 +0100
+++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Jan 31 10:49:17 2023 +0100
@@ -41,7 +41,7 @@
 \<close>
 text \<open>... and  let us differentiate the term t:\<close>
 ML \<open>
-val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)";
+val t = ParseC.parse_test ctxt "d_d x (x\<up>2 + x + y)";
 
 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
@@ -80,10 +80,10 @@
 text \<open>We have already seen conditional rewriting above when we used the rule
   diff_const; let us try:\<close>
 ML \<open>
-val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)";
+val t1 = ParseC.parse_test ctxt "d_d x (a*BC*x*z)";
 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t1;
 
-val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)";
+val t2 = ParseC.parse_test ctxt "d_d x (a*BC*y*z)";
 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t2;
 \<close>
 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, 
@@ -98,7 +98,7 @@
 \<close>
 ML \<open>
 (*show_brackets := true; TODO*)
-val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
+val t0 = ParseC.parse_test ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
 (*show_brackets := false;*)
 \<close>
 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
@@ -147,11 +147,11 @@
 \<close>
 ML \<open>
 (*show_brackets := false; TODO*)
-val t1 = TermC.parseNEW' ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
+val t1 = ParseC.parse_test ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term t;
 \<close>
 ML \<open>
-val t2 = TermC.parseNEW' ctxt 
+val t2 = ParseC.parse_test ctxt 
   "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t;
 \<close>
@@ -185,7 +185,7 @@
 
 subsection \<open>What already works\<close>
 ML \<open>
-val t2 = TermC.parseNEW' ctxt 
+val t2 = ParseC.parse_test ctxt 
   "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real";
 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true rls_p_33 t2; UnparseC.term t;
 \<close>
@@ -225,7 +225,7 @@
 
 subsection \<open>This does not yet work\<close>
 ML \<open>
-val t = TermC.parseNEW' ctxt 
+val t = ParseC.parse_test ctxt 
   "(2*a - 5*b) * (2*a + 5*b)";
 Rewrite.rewrite_set_ ctxt true rls_p_33 t; UnparseC.term t;
 \<close>