diff -r 0d22a6bf1fc6 -r 0ee698b0a703 test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 20 14:37:56 2021 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 27 11:21:14 2021 +0200
@@ -351,7 +351,7 @@
 \  (((Try (Rewrite_Set ordne_alphabetisch False)) #>     \
 \    (Try (Rewrite_Set fasse_zusammen False)) #>     \
 \    (Try (Rewrite_Set verschoenere False))) t_t)"
-val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
+val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
 TermC.atomty sc;
 
 "----------- me simplification.for_polynomials.with_minus";
@@ -468,7 +468,7 @@
 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #>  \
 \            (Try (Repeat (Calculate ''PLUS''))) #>  \
 \            (Try (Repeat (Calculate ''MINUS''))))) e_e)"
-val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
+val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
 TermC.atomty sc;
 
 "----------- pbl polynom probe -----------------------------------";