1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 20 14:37:56 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 27 11:21:14 2021 +0200
     1.3 @@ -351,7 +351,7 @@
     1.4  \  (((Try (Rewrite_Set ordne_alphabetisch False)) #>     \
     1.5  \    (Try (Rewrite_Set fasse_zusammen False)) #>     \
     1.6  \    (Try (Rewrite_Set verschoenere False))) t_t)"
     1.7 -val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
     1.8 +val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
     1.9  TermC.atomty sc;
    1.10  
    1.11  "----------- me simplification.for_polynomials.with_minus";
    1.12 @@ -468,7 +468,7 @@
    1.13  \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #>  \
    1.14  \            (Try (Repeat (Calculate ''PLUS''))) #>  \
    1.15  \            (Try (Repeat (Calculate ''MINUS''))))) e_e)"
    1.16 -val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
    1.17 +val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
    1.18  TermC.atomty sc;
    1.19  
    1.20  "----------- pbl polynom probe -----------------------------------";