1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 18:39:02 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Jul 20 14:37:56 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 Thm.term_of o the o (TermC.parse thy)) str;
1.8 +val sc = (inst_abs o (TermC.parseNEW'' 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 Thm.term_of o the o (TermC.parse thy)) str;
1.17 +val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
1.18 TermC.atomty sc;
1.19
1.20 "----------- pbl polynom probe -----------------------------------";