
diff -r b2ff1902420f -r 06ec8abfd3bc test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy
--- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Wed Jan 11 09:23:18 2023 +0100
+++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Wed Jan 11 11:38:01 2023 +0100
@@ -68,7 +68,8 @@
   http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html
 \<close>
 ML \<open>
-val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; UnparseC.term t;
+val t = @{term "%x. x^2 + x + y"};
+TermC.atom_write_detail @{context} t; UnparseC.term_in_ctxt @{context} t;
 \<close>
 text \<open>Since this notation does not conform to present high-school matheatics
   ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation




