diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Knowledge/Diff.thy
--- a/src/Tools/isac/Knowledge/Diff.thy	Sun Oct 09 09:01:29 2022 +0200
+++ b/src/Tools/isac/Knowledge/Diff.thy	Wed Oct 19 10:43:04 2022 +0200
@@ -244,7 +244,7 @@
 (** CAS-commands **)
 
 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
-(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
+(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)");
    val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
    *)
 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
@@ -390,7 +390,7 @@
 ML \<open>
 
 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
-(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
+(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)");
    val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
    *)
 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =