1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  (*.function for handling the cas-input "Simplify (2*a + 3*a)":
     1.6     make a model which is already in ctree-internal format.*)
     1.7 -(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
     1.8 +(* val (h,argl) = strip_comb (TermC.parse_test @{context} "Simplify (2*a + 3*a)");
     1.9     val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify"))) 
    1.10  				  "Simplify (2*a + 3*a)");
    1.11     *)