1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4  (** CAS-commands **)
     1.5  
     1.6  (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
     1.7 -(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
     1.8 +(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)");
     1.9     val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
    1.10     *)
    1.11  fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
    1.12 @@ -390,7 +390,7 @@
    1.13  ML \<open>
    1.14  
    1.15  (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
    1.16 -(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
    1.17 +(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)");
    1.18     val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
    1.19     *)
    1.20  fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =